Certified Kruskal’s Tree Theorem

Christian Sternagel

Journal of Formalized Reasoning 7(1), pp. 45 – 62, 2014.


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.


  PDF |    doi:10.6092/issn.1972-5787/4213


author = "Christian Sternagel",
title = "Certified Kruskal's Tree Theorem"
journal = "Journal of Formalized Reasoning",
volume = 7,
number = 1,
pages = "45--62",
year = 2014,
doi = "10.6092/issn.1972-5787/4213"
Nach oben scrollen