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.

  1. 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:
  2. 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.
  3. 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.

FORTissimo will start on September 1, 2017 and run for three years.

Members


Current Members

  • Jamie Hochrainer
  • Johannes Koch
  • Alexander Lochmann
  • Aart Middeldorp (coordination)
  • Fabian Mitterwallner

Former Members

  • Bertram Felgenhauer
  • Fabian Mitterwallner
  • T. V. H. Prathamesh
  • Franziska Rapp
  • Kei Shirakizawa (guest)

 

FWF project number
P30301

  Contact
aart.middeldorp@uibk.ac.at

Publications

  • A Verified Decision Procedure for the First-Order Theory of Rewriting for Linear Variable-Separated Rewrite Systems
    Alexander Lochmann, Aart Middeldorp, Fabian Mitterwallner, Bertram Felgenhauer
    10th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2021),   pp. 250 – 263, 2021.
  • Formalized Proofs of the Infinity and Normal Form Predicates in the First-Order Theory of Rewriting
    Alexander Lochmann, Aart Middeldorp
    26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, LCNS 12079, pp. 25 – 40, 2020.
  • 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
    8th ACM SIGPLAN International Conference on Certified Programs and Proofs,   pp. 132 – 143, 2019.
  • 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, Franziska Rapp
    Proceedings of the 7th International Workshop on Confluence (IWC 2018),   pp. 46 – 50, 2018.
  • FORT 2.0
    Franziska Rapp, Aart Middeldorp
    Proceedings of the 9th International Joint Conference on Automated Reasoning, Lecture Notes in Artificial Intelligence 10900, pp. 81 – 88, 2018.
Nach oben scrollen