Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: "First-Order Rewriting" and "P...

Email Gateway (Apr 13 2025 at 19:55):

From: Tobias Nipkow <nipkow@in.tum.de>
First-Order Rewriting
René Thiemann, Christian Sternagel, Christina Kirk, Martin Avanzini, Bertram
Felgenhauer, Julian Nagele, Thomas Sternagel, Sarah Winkler and Akihisa Yamada

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.

https://www.isa-afp.org/entries/First_Order_Rewriting.html

Proof Terms for Term Rewriting
Christina Kirk

Proof terms are first-order terms that represent reductions in term rewriting.
They were initially introduced in TeReSe by van Oostrom and de Vrijer to study
equivalences of reductions in left-linear rewrite systems. This entry formalizes
proof terms for multi-steps in first-order term rewrite systems. We define
simple proof terms (i.e., without a composition operator) and establish the
correspondence to multi-steps: each proof term represents a multi-step with the
same source and target, and every multi-step can be expressed as a proof term.
The formalization moreover includes operations on proof terms, such as
residuals, join, and deletion and a method for labeling proof term sources to
identify overlaps between two proof terms.
This formalization is part of the Isabelle Formalization of Rewriting (IsaFoR)
and is an essential component of several formalized confluence and commutation
results involving multi-steps.

https://www.isa-afp.org/entries/Proof_Terms_Term_Rewriting.html

Enjoy!

smime.p7s

Last updated: May 30 2025 at 04:27 UTC