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
Topics
Session FO_Theory_Rewriting
- Utils
- Multihole_Context
- Ground_MCtxt
- Bot_Terms
- Saturation
- Rewriting
- LV_to_GTT
- NF
- Tree_Automata_Derivation_Split
- TA_Clousure_Const
- Type_Instances_Impl
- NF_Impl
- Context_Extensions
- FOR_Certificate
- Lift_Root_Step
- Context_RR2
- GTT_RRn
- FOL_Extra
- FOR_Semantics
- FOR_Check
- FOR_Check_Impl