Email Gateway (Feb 10 2022 at 17:24): Email Gateway (Feb 10 2022 at 17:24):From: Tobias Nipkow <nipkow@in.tum.de>
First-Order Theory of Rewriting
Alexander Lochmann and Bertram Felgenhauer
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.
https://www.isa-afp.org/entries/FO_Theory_Rewriting.html
Enjoy!
smime.p7s
Last updated: Jan 04 2025 at 20:18 UTC