A formalization of the Knuth-Bendix(-Huet) critical pair theorem

DOI10.1007/s10817-010-9165-2zbMath1207.68338DBLPjournals/jar/GaldinoA10OpenAlexW1969006866WikidataQ58001438 ScholiaQ58001438MaRDI QIDQ616850

Sumit K. Garg

Publication date: 12 January 2011

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-010-9165-2

zbMATH Keywords

term rewriting systemsabstract reduction systemsPVScritical pair theoremformalization of theorems

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Related Items (5)

Confluence of orthogonal term rewriting systems in the prototype verification system ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Checking overlaps of nominal rewriting rules ⋮ Completeness in PVS of a nominal unification algorithm

Uses Software

• ACL2
• PVS
• NQTHM
• CoLoR
• SAEPTUM
• FELIX
• RRL

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• More Church-Rosser proofs (in Isabelle/HOL)
• Formal proofs about rewriting using ACL2
• Some lambda calculus and type theory formalized
• Certification of Automated Termination Proofs
• A mechanical proof of the Church-Rosser theorem
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• Term Rewriting and All That
• Residual theory in λ-calculus: a formal development
• A PVS Theory for Term Rewriting Systems

This page was built for publication: A formalization of the Knuth-Bendix(-Huet) critical pair theorem