Certified Kruskal's Tree Theorem

Authors

  • Christian Sternagel University of Innsbruck

DOI:

https://doi.org/10.6092/issn.1972-5787/4213

Keywords:

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

Abstract

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.

Downloads

Published

2014-07-17

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

Issue

Section

Articles