Certified Kruskal's Tree Theorem

DOI10.6092/ISSN.1972-5787/4213zbMath1426.68289OpenAlexW1520750303MaRDI QIDQ5195254

Christian Sternagel

Publication date: 18 September 2019

Full work available at URL: https://doaj.org/article/58453159a0ca4057ac9953d74dbc833d

zbMATH Keywords

Kruskal'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)

A Mechanized Proof of Higman’s Lemma by Open Induction ⋮ Higman’s Lemma and Its Computational Content

Uses Software

• HOL
• Unnamed Item
• Unnamed Item

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