Formalizing Knuth-Bendix Orders and Knuth-Bendix Completion

DOI10.4230/LIPIcs.RTA.2013.287zbMath1356.68201OpenAlexW2272899792MaRDI QIDQ2958390

Christian Sternagel, René Thiemann

Publication date: 1 February 2017

Full work available at URL: https://doi.org/10.4230/lipics.rta.2013.287

zbMATH Keywords

completionconfluenceterminationcertification

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Grammars and rewriting systems (68Q42)

Related Items

Unnamed Item ⋮ Formalization of the resolution calculus for first-order logic ⋮ Certified Kruskal’s Tree Theorem ⋮ Order Reconfiguration under Width Constraints ⋮ A Mechanized Proof of Higman’s Lemma by Open Induction ⋮ Unnamed Item ⋮ Certified equational reasoning via ordered completion

Uses Software

• Isabelle
• Isabelle/HOL
• CeTA
• mkbTT
• KBCV
• Well Quasi Orders
• Archive Formal Proofs