First-Order Rewriting (Q7361314)
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 First_Order_Rewriting
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | First-Order Rewriting |
AFP entry First_Order_Rewriting |
Statements
13 April 2025
0 references
René Thiemann
0 references
Christian Sternagel
0 references
Christina Kirk
0 references
Martin Avanzini
0 references
Bertram Felgenhauer
0 references
Julian Nagele
0 references
Thomas Sternagel
0 references
Sarah Winkler
0 references
Akihisa Yamada
0 references
First-Order Rewriting (English)
0 references
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.
0 references
