First-Order Theory of Rewriting (Q7361032)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry FO_Theory_Rewriting
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | First-Order Theory of Rewriting |
AFP entry FO_Theory_Rewriting |
Statements
2 February 2022
0 references
Alexander Lochmann
0 references
Bertram Felgenhauer
0 references
First-Order Theory of Rewriting (English)
0 references
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.
0 references
