Abstract

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.

BibTeX

@inproceedings{CS-CPP13,
  author      = "Christian Sternagel",
  title       = "Certified Kruskal's Tree Theorem", 
  booktitle   = "Proceedings of the 3rd International Conference on Certified Programs and Proofs", 
  series      = "LNCS",
  volume      = 830,
  pages       = "178--193",
  year        = 2013
}