Certified Kruskal's Tree Theorem
This article presents the first formalization of Kurskal's tree theorem in aproof assistant. The Isabelle/HOL development is along the lines of Nash-Williams' original minimal bad sequence argument for proving the treetheorem. Along the way, proofs of Dickson's lemma and Higman's...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
University of Bologna
2014-07-01
|
| Series: | Journal of Formalized Reasoning |
| Subjects: | |
| Online Access: | http://jfr.unibo.it/article/view/4213 |
| _version_ | 1811218153677520896 |
|---|---|
| author | Christian Sternagel |
| author_facet | Christian Sternagel |
| author_sort | Christian Sternagel |
| collection | DOAJ |
| description | This article presents the first formalization of Kurskal's tree theorem in aproof assistant. The Isabelle/HOL development is along the lines of Nash-Williams' original minimal bad sequence argument for proving the treetheorem. Along the way, proofs of Dickson's lemma and Higman's lemma, as well as some technical details of the formalization are discussed. |
| first_indexed | 2024-04-12T07:05:54Z |
| format | Article |
| id | doaj.art-58453159a0ca4057ac9953d74dbc833d |
| institution | Directory Open Access Journal |
| issn | 1972-5787 |
| language | English |
| last_indexed | 2024-04-12T07:05:54Z |
| publishDate | 2014-07-01 |
| publisher | University of Bologna |
| record_format | Article |
| series | Journal of Formalized Reasoning |
| spelling | doaj.art-58453159a0ca4057ac9953d74dbc833d2022-12-22T03:42:48ZengUniversity of BolognaJournal of Formalized Reasoning1972-57872014-07-0171456210.6092/issn.1972-5787/42134066Certified Kruskal's Tree TheoremChristian Sternagel0University of InnsbruckThis article presents the first formalization of Kurskal's tree theorem in aproof assistant. The Isabelle/HOL development is along the lines of Nash-Williams' original minimal bad sequence argument for proving the treetheorem. Along the way, proofs of Dickson's lemma and Higman's lemma, as well as some technical details of the formalization are discussed.http://jfr.unibo.it/article/view/4213almost-full relationswell-quasi-ordersDickson's lemmaHIgman's lemmaKruskal's tree theoremminimal bad sequences |
| spellingShingle | Christian Sternagel Certified Kruskal's Tree Theorem Journal of Formalized Reasoning almost-full relations well-quasi-orders Dickson's lemma HIgman's lemma Kruskal's tree theorem minimal bad sequences |
| title | Certified Kruskal's Tree Theorem |
| title_full | Certified Kruskal's Tree Theorem |
| title_fullStr | Certified Kruskal's Tree Theorem |
| title_full_unstemmed | Certified Kruskal's Tree Theorem |
| title_short | Certified Kruskal's Tree Theorem |
| title_sort | certified kruskal s tree theorem |
| topic | almost-full relations well-quasi-orders Dickson's lemma HIgman's lemma Kruskal's tree theorem minimal bad sequences |
| url | http://jfr.unibo.it/article/view/4213 |
| work_keys_str_mv | AT christiansternagel certifiedkruskalstreetheorem |