Certified Kruskal's Tree Theorem

Christian Sternagel


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.


almost-full relations; well-quasi-orders; Dickson's lemma; HIgman's lemma; Kruskal's tree theorem; minimal bad sequences

Full Text:

PDF (English)

DOI: 10.6092/issn.1972-5787/4213

Copyright (c) 2014 Christian Sternagel

Creative Commons License
This work is licensed under a Creative Commons Attribution 3.0 Unported License.