Certified Kruskal’s tree theorem
Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre órdenes titulado Certified Kruskal’s tree theorem.
Su autor es Christian Sternagel (del Japan Advanced Institute of Science and Technology).
Su resumen es
This paper gives the first formalization of Kruskal’s tree theorem in a proof assistant. More concretely, an Isabelle/HOL development of Nash-Williams’ minimal bad sequence argument for proving the tree theorem is presented. Along the way, the proofs of Dickson’s lemma and Higman’s lemma are discussed.
El trabajo se presentará en el CPP 2013 (3rd International Conference on Certified Programs and Proofs).
El código de las correspondientes teorías en Isabelle/HOL se encuentra aquí.