On-line Lecture by Dr. Aart Middeldorp on September 24, 2021(For Students of Nagoya University only)

Date & Time：　September 24,2021 13:00-16:15
Place:　Zoom
speaker:Aart Middeldorp
Topic： First-Order Theory of Rewriting: Automation, Formalization, Certification

Summary:
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.

Contact:価値創造研究センター事務室 <office-fvcrcnu@i.nagoya-u.ac.jp>
: