Certified Kruskal's Tree Theorem
Keywords:almost-full relations, well-quasi-orders, Dickson's lemma, HIgman's lemma, Kruskal's tree theorem, minimal bad sequences
AbstractThis 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.
How to Cite
Sternagel, C. (2014). Certified Kruskal’s Tree Theorem. Journal of Formalized Reasoning, 7(1), 45–62. https://doi.org/10.6092/issn.1972-5787/4213
Copyright (c) 2014 Christian Sternagel
Copyrights and publishing rights of all the texts on this journal belong to the respective authors without restrictions.