2026-08-18T03:34:33Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:4068 2024-03-06T10:34:47Z ddc:004 open_access

Formalizing Knuth-Bendix Orders and Knuth-Bendix Completion Sternagel, Christian Thiemann, René certification completion confluence termination We present extensions of our Isabelle Formalization of Rewriting that cover two historically related concepts: the Knuth-Bendix order and the Knuth-Bendix completion procedure. The former, besides being the first development of its kind in a proof assistant, is based on a generalized version of the Knuth-Bendix order. We compare our version to variants from the literature and show all properties required to certify termination proofs of TRSs. The latter comprises the formalization of important facts that are related to completion, like Birkhoff's theorem, the critical pair theorem, and a soundness proof of completion, showing that the strict encompassment condition is superfluous for finite runs. As a result, we are able to certify completion proofs. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Christian Sternagel and René Thiemann 2013 Is Part Of LIPIcs, Volume 21, 24th International Conference on Rewriting Techniques and Applications (RTA 2013) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.RTA.2013.287 urn:nbn:de:0030-drops-40685 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2013.287 eng https://creativecommons.org/licenses/by/3.0/legalcode