First-Order Rewriting

René Thiemann 📧, Christian Sternagel 📧, Christina Kirk 📧, Martin Avanzini 📧, Bertram Felgenhauer 📧, Julian Nagele 📧, Thomas Sternagel, Sarah Winkler 📧 and Akihisa Yamada 📧

April 13, 2025

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.

License

BSD License

Topics

Session First_Order_Rewriting

Depends on

Used by

Cite

× 
@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},
}
Download