cl-banner

Certified Kruskal's Tree Theorem

Christian Sternagel

Proceedings of the 3rd International Conference on Certified Programs and Proofs (CPP 2013), Lecture Notes in Computer Science 8307, pp. 178 – 193, 2013

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.

 

  PDF |    doi:10.1007/978-3-319-03545-1_12

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
}
Nach oben scrollen