Reseña: Certified Kruskal’s tree theorem
Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL titulado Certified Kruskal’s tree theorem
Su autor es Christian Sternagel (del Computational Logic Research Group en la Univ. de Insbruck, Austria).
Su resumen es
This article presents the first formalization of Kurskal’s tree theorem in a proof assistant. The Isabelle/HOL development is along the lines of Nash-Williams’ original minimal bad sequence argument for proving the tree theorem. Along the way, proofs of Dickson’s lemma and Higman’s lemma, as well as some technical details of the formalization are discussed.
El trabajo se ha publicado en Journal of Formalized Reasoning.
El código de las correspondientes teorías en Isabelle/HOL se encuentra aquí.