Reseña: A new and formalized proof of abstract completion
Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL titulado A new and formalized proof of abstract completion.
Sus autores son
- Nao Hirokawa (del Japan Advanced Institute of Science and Technology, Japón),
- Aart Middeldorp (de la University of Innsbruck, Austria) y
- Christian Sternagel (de la University of Innsbruck, Austria)-
Su resumen es
Completion is one of the most studied techniques in term rewriting. We present a new proof of the correctness of abstract completion that is based on peak decreasingness, a special case of decreasing diagrams. Peak decreasingness replaces Newman’s Lemma and allows us to avoid proof orders in the correctness proof of completion. As a result, our proof is simpler than the one presented in textbooks, which is confirmed by our Isabelle/HOL formalization. Furthermore, we show that critical pair criteria are easily incorporated in our setting.
El trabajo se presentará el martes 15 de julio en el ITP 2014 (5th Conference on Interactive Theorem Proving).
El código de las correspondientes teorías en Isabelle/HOL es encuentra aquí.