LIPIcs.RTA.2013.287.pdf
- Filesize: 0.54 MB
- 16 pages
Document
Formalizing Knuth-Bendix Orders and Knuth-Bendix Completion
Authors
-
Part of:
Volume:
24th International Conference on Rewriting Techniques and Applications (RTA 2013)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Rewriting Techniques and Applications (RTA) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2013-06-24
Cite As Get BibTex
Christian Sternagel and René Thiemann. Formalizing Knuth-Bendix Orders and Knuth-Bendix Completion. In 24th International Conference on Rewriting Techniques and Applications (RTA 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 21, pp. 287-302, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
https://doi.org/10.4230/LIPIcs.RTA.2013.287
Abstract
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.
Subject Classification
Keywords
- certification
- completion
- confluence
- termination
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads