Certified Kruskal's Tree Theorem

Journal of Formalized Reasoning

Christian Sternagel

关键词: almost-full relations;    well-quasi-orders;    Dickson's lemma;    HIgman's lemma;    Kruskal's tree theorem;    minimal bad sequences;   

DOI  :  10.6092/issn.1972-5787/4213

学科分类：计算机科学（综合）

来源: Universita degli Studi di Bologna

【 摘 要 】

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.

【 授权许可】

CC BY