### 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

- Computer science/Automata and formal languages
- Logic/Rewriting
- Logic/Proof theory

### 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

### Depends on

- First-Order Logic According to Fitting
- Regular Tree Relations

### Auto-related entries

- MLSS Decision Procedure
- Landau Symbols

## Cite

×

FO_Theory_Rewriting-AFP

    @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:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Feb 10, 2022 : Isabelle2021-1