Skip to main content
Conference Proceedings

Certified Kruskal's tree theorem

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (2013) 8307 LNCS 178-193
DOI: 10.1007/978-3-319-03545-1_12
2Citations
Citations of this article
3Readers
Mendeley users who have this article in their library.
Get full text

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. © Springer International Publishing 2013.

Author supplied keywords

Cite

CITATION STYLE

APA

Sternagel, C. (2013). Certified Kruskal’s tree theorem. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8307 LNCS, pp. 178–193). https://doi.org/10.1007/978-3-319-03545-1_12

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free