First-Order Theory of Rewriting

Alexander Lochmann 📧 and Bertram Felgenhauer

February 2, 2022

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Abstract

The first-order theory of rewriting (FORT) is a decidable theory for linear variable-separated rewrite systems. The decision procedure is based on tree automata technique and an inference system presented in "Certifying Proofs in the First-Order Theory of Rewriting". This AFP entry provides a formalization of the underlying decision procedure. Moreover it allows to generate a function that can verify each inference step via the code generation facility of Isabelle/HOL. Additionally it contains the specification of a certificate language (that allows to state proofs in FORT) and a formalized function that allows to verify the validity of the proof. This gives software tool authors, that implement the decision procedure, the possibility to verify their output.

License

BSD License

Topics

Session FO_Theory_Rewriting

Depends on

Cite

× 
@article{FO_Theory_Rewriting-AFP,
  author  = {Alexander Lochmann and Bertram Felgenhauer},
  title   = {First-Order Theory of Rewriting},
  journal = {Archive of Formal Proofs},
  month   = {February},
  year    = {2022},
  note    = {\url{https://isa-afp.org/entries/FO_Theory_Rewriting.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: