Certified Kruskal’s Tree Theorem

DOI10.1007/978-3-319-03545-1_12zbMath1426.68288OpenAlexW2175970794MaRDI QIDQ2938047

Christian Sternagel

Publication date: 13 January 2015

Published in: Certified Programs and Proofs (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-03545-1_12

zbMATH Keywords

Dickson's lemmaHigman's lemmawell-quasi-ordersKruskal's tree theoremminimal bad sequences

Mathematics Subject Classification ID

Foundations of classical theories (including reverse mathematics) (03B30) Second- and higher-order arithmetic and fragments (03F35) Formalization of mathematics in connection with theorem provers (68V20)

Related Items (2)

Well Quasi-orders and the Functional Interpretation ⋮ A formalisation of the Myhill-Nerode theorem based on regular expressions

Uses Software

• Isabelle
• Isabelle/HOL
• HOL

Cites Work

• Unnamed Item
• Unnamed Item
• Proof pearl: a formal proof of Higman's lemma in ACL2
• Proving open properties by induction
• Simple termination of rewrite systems
• Isabelle/HOL. A proof assistant for higher-order logic
• An intuitionistic proof of Kruskal's theorem
• Stop When You Are Almost-Full
• Formalizing Knuth-Bendix Orders and Knuth-Bendix Completion
• A Formalisation of the Myhill-Nerode Theorem Based on Regular Expressions (Proof Pearl)
• Well-Quasi-Ordering, The Tree Theorem, and Vazsonyi's Conjecture
• Types for Proofs and Programs
• Ordering by Divisibility in Abstract Algebras

This page was built for publication: Certified Kruskal’s Tree Theorem