Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: First-Order Theory of Rewriting


view this post on Zulip 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: Jul 15 2022 at 23:21 UTC