Formalizing Knuth-Bendix Orders and Knuth-Bendix Completion

Christian Sternagel and René Thiemann

Proceedings of the 24th International Conference on Rewriting Techniques and Applications (RTA 2013), Leibniz International Proceedings in Informatics 21, pp. 287 – 302, 2013.


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.


  PDF |    doi:10.4230/LIPIcs.RTA.2013287  |  © Creative Commons License - NC - ND


author = "Christian Sternagel and Ren{\'e} Thiemann",
title = "Formalizing Knuth-Bendix Orders and Knuth-Bendix Completion",
booktitle = "Proceedings of the 24th International Conference on Rewriting
Techniques and Applications",
editor = "Femke van Raamsdonk",
series = "Leibniz International Proceedings in Informatics",
volume = 21,
pages = "287--302",
year = 2013,
doi = "10.4230/LIPIcs.RTA.2013.287"
Nach oben scrollen