Reseña: Formalizing Knuth-Bendix orders and Knuth-Bendix completion
Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre sistemas de reescritura titulado Formalizing Knuth-Bendix orders and Knuth-Bendix completion.
Sus autores son Christian Sternagel (del Instituto japonés de ciencias y tecnología) y René Thiemann (de la Univ. de Innsbruck, Austria).
El trabajo se presentará en junio en la RTA 2013 (24th International Conference
on Rewriting Techniques and Applications).
Su resumen es
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.
El código con las correspondientes teorías Isabelle se encuentra en la versión 2.10 de IsaFoR/CeTA.