Abstract

This entry, derived from the Isabelle Formalization of Rewriting (IsaFoR), provides a formalized foundation for first-order term rewriting. This serves as the basis for the certifier CeTA, which is generated from IsaFoR and verifies termination, confluence, and complexity proofs for term rewrite systems (TRSs). This formalization covers fundamental results for term rewriting, as presented in the foundational textbooks by Baader and Nipkow and TeReSe. These include:

• Various types of rewrite steps, such as root, ground, parallel, and multi-steps.


• Special cases of TRSs, such as linear and left-linear TRSs.


• A definition of critical pairs and key results, including the critical pair lemma.


• Orthogonality, notably that weak orthogonality implies confluence.


• Executable versions of relevant definitions, such as parallel and multi-step rewriting.

BibTeX

@article{First_Order_Rewriting-AFP,
  author  = {René Thiemann and Christian Sternagel and Christina Kirk and Martin Avanzini and Bertram Felgenhauer and Julian Nagele and Thomas Sternagel and Sarah Winkler and Akihisa Yamada},
  title   = {First-Order Rewriting},
  journal = {Archive of Formal Proofs},
  month   = {April},
  year    = {2025},
  note    = {\url{https://isa-afp.org/entries/First_Order_Rewriting.html},
             Formal proof development},
  ISSN    = {2150-914x},
}