FORTissimo: Automating the First-Order Theory of Rewriting
FORTissimo is about the first-order theory of rewriting, which is a decidable theory for left-linear right-ground rewrite systems in which well-known properties like confluence, normalization and termination are expressible. The decision procedure for this theory is based on tree automata techniques and a first implementation was conducted by Franziska Rapp during her master studies. The resulting tool FORT is equipped with a synthesis mode to generate rewrite systems that satisfy properties expressible in the first-order theory of rewriting.
The aim of this project is to formalize the decision procedure in the proof assistant Isabelle/HOL such that the output of FORT can be certified. Moreover, the expressiveness and the performance of FORT should be increased, and its limitations better understood. More concretely, the project has the following three main objectives:
- Formalize the basic properties of automata on n-ary relations (cylindrification, projection) and ground tree transducers in Isabelle/HOL. Develop suitable certificates that can be produced by FORT and checked by the certifier obtained from the formalization in Isabelle via code generation.
- Improve the performance of FORT by adopting and developing state-of-the-art tree automata techniques. Investigate methods for formula normalization in order to speed up the computation of intermediate automata. Adopt parallel programming techniques to further improve the efficiency of FORT.
- Improve the expressiveness of FORT by adding support for combinations of rewrite systems and the generation of witnesses for existentially quantified variables. Investigate to what extent properties on open terms can be simulated in FORT, and whether certain fragments of the first-order theory of rewriting are decidable for larger classes of rewrite systems.
Members
- Bertram Felgenhauer
- Jamie Hochrainer
- Johannes Koch
- Alexander Lochmann
- Aart Middeldorp (coordination)
- Fabian Mitterwallner
- Johannes Niederhauser
- T. V. H. Prathamesh
- Franziska Rapp
- Kei Shirakizawa (guest)
FWF
FORTissimo is supported by FWF (P30301) from September 1, 2017 until March 1, 2022.Contact
aart middeldorp at uibk dot ac dot atPublications
Formalized Signature Extension Results for Equivalence
Alexander Lochmann, Fabian Mitterwallner, and Aart Middeldorp
Proceedings of the 11th International Workshop on Confluence (IWC 2022),
pp. 42 – 47, 2022
Reducing Rewrite Properties to Properties on Ground Terms
Alexander Lochmann
Archive of Formal Proofs, 2022
First-Order Theory of Rewriting
Alexander Lochmann and Bertram Felgenhauer
Archive of Formal Proofs, 2022
Regular Tree Relations
Alexander Lochmann, Bertram Felgenhauer, Christian Sternagel, René
Thiemann, and Thomas Sternagel
Archive of Formal Proofs, 2021
Formalized Signature Extension Results for Confluence, Commutation and
Unique Normal Forms
Alexander Lochmann, Fabian Mitterwallner, and Aart Middeldorp
Proceedings of the 10th International Workshop on Confluence (IWC 2021),
pp. 25 – 30, 2021
supporting website
Certifying Proofs in the First-Order Theory of Rewriting
Fabian Mitterwallner, Alexander Lochmann, Aart Middeldorp, and Bertram
Felgenhauer
Proceedings of the 27th International Conference on Tools and Algorithms
for the Construction and Analysis of Systems (TACAS 2021),
Lecture Notes in Computer Science 12652, pp. 127 – 144, 2021
supporting website
A Verified Decision Procedure for the First-Order Theory of Rewriting
for Linear Variable-Separated Rewrite Systems
Alexander Lochmann, Aart Middeldorp, Fabian Mitterwallner, and Bertram
Felgenhauer
Proceedings of the 10th ACM SIGPLAN International Conference on Certified
Programs and Proofs (CPP 2021), pages 250 – 263, 2021
supporting website
Formalized Proofs of the Infinity and Normal Form Predicates in the
First-Order Theory of Rewriting
Alexander Lochmann and Aart Middeldorp
Proceedings of the 26th International Conference on Tools and Algorithms
for the Construction and Analysis of Systems (TACAS 2020),
Lecture Notes in Computer Science 12079, pp. 25 – 40, 2020
supporting website
A Verified Ground Confluence Tool for Linear Variable-Separated Rewrite
Systems in Isabelle/HOL
Bertram Felgenhauer, Aart Middeldorp, T. V. H. Prathamesh, and Franziska
Rapp
Proceedings of the 8th ACM SIGPLAN International Conference on Certified
Programs and Proofs (CPP 2019), ACM, pp. 132 – 143, 2019
supporting website
Minsky Machines
Bertram Felgenhauer
Archive of Formal Proofs, 2018
Towards a Verified Decision Procedure for Confluence of Ground Term
Rewrite Systems in Isabelle/HOL
Bertram Felgenhauer, Aart Middeldorp, T. V. H. Prathamesh, and Franziska
Rapp
Proceedings of the 7th International Workshop on Confluence (IWC 2018),
pp. 46 – 50, 2018
supporting website
FORT 2.0
Franziska Rapp and Aart Middeldorp
Proceedings of the 9th International Joint Conference on Automated
Reasoning (IJCAR-9),
Lecture Notes in Artificial Intelligence 10900, pp. 81 – 88, 2018