2021年9月24日（金）外国人客員教員Aart Middeldorp先生によるZoom授業を開催いたします（対象 本学学生）

日時：　 9月24日（金）3限、4限
場所:　  Zoom
話者	Aart Middeldorp
題目：   First-Order Theory of Rewriting: Automation, Formalization, Certification
概要：

In the first half of this presentation I will present FORT-h, a convenient software tool that implements a decision procedure for the first-order
theory of rewriting, for the class of linear, variable-separated term rewrite systems. In this theory important properties of rewrite systems
like termination, confluence and normalization are readily expressed. The decision procedure is based on tree automata techniques and has been
formalized in the proof assistant Isabelle/HOL. The latest version of FORT-h is capable of producing certificates which are verified by FORTIFY,
a certifier that is obtained from the formalization in Isabelle/HOL via code generation. Besides deciding properties, FORT-h is equipped with a
synthesis mode for automatically finding rewrite systems that satisfy properties expressible in the first-order theory.

The decision procedure is based on bottom-up tree automata and ground tree transducers. In the second half of the presentation I will present in some
detail the various operations and closure properties that make up the decision procedure.

The presentation is based on joint work with Bertram Felgenhauer, Jamie Hochrainer, Johannes Koch, Alexander Lochmann, Fabian Mitterwallner,
T.V.H. Prathamesh, and Franziska Rapp.


お問合わせ先：価値創造研究センター事務室 office-fvcrcnu@i.nagoya-u.ac.jp