Certified Kruskal's Tree Theorem
Sternagel, Christian
Journal of Formalized Reasoning, Tome 7 (2014), / Harvested from Journal of Formalized Reasoning
Link
Link

This article presents the first formalization of Kurskal's tree theorem in aproof assistant. The Isabelle/HOL development is along the lines of Nash-Williams' original minimal bad sequence argument for proving the treetheorem. Along the way, proofs of Dickson's lemma and Higman's lemma, as well as some technical details of the formalization are discussed.

Publié le : 2014-01-01
DOI : https://doi.org/10.6092/issn.1972-5787/4213 
@article{4213,
     title = {Certified Kruskal's Tree Theorem},
     journal = {Journal of Formalized Reasoning},
     volume = {7},
     year = {2014},
     doi = {10.6092/issn.1972-5787/4213},
     language = {EN},
     url = {http://dml.mathdoc.fr/item/4213}
}

Sternagel, Christian. Certified Kruskal's Tree Theorem. Journal of Formalized Reasoning, Tome 7 (2014) . doi : 10.6092/issn.1972-5787/4213. http://gdmltest.u-ga.fr/item/4213/