Higman’s Lemma and Its Computational Content

DOI10.1007/978-3-319-29198-7_11zbMath1439.03099OpenAlexW2461293012MaRDI QIDQ3305561

Monika Seisenberger, Franziskus Wiesnet, Helmut Schwichtenberg

Publication date: 7 August 2020

Published in: Advances in Proof Theory (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-29198-7_11

zbMATH Keywords

program extractionHigman's lemmainductive definitionsminimal bad sequence

Mathematics Subject Classification ID

Permutations, words, matrices (05A05) Structure of proofs (03F07) Complexity of proofs (03F20)

Related Items (1)

A Mechanized Proof of Higman’s Lemma by Open Induction

Uses Software

• Coq
• Minlog

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Proof pearl: a formal proof of Higman's lemma in ACL2
• Ordinal recursive bounds for Higman's theorem
• Proof-theoretic investigations on Kruskal's theorem
• Logic, language and computation. Festschrift in Honor of Satoru Takasu
• A characterisation of multiply recursive functions with Higman's lemma.
• Well quasi-ordered sets
• An intuitionistic proof of Kruskal's theorem
• A Constructive Proof of the Topological Kruskal Theorem
• Minlog - A Tool for Program Extraction Supporting Algebras and Coalgebras
• Proofs and Computations
• Ramsey's Theorem and the Pigeonhole Principle in Intuitionistic Mathematics
• Ein in der reinen Zahlentheorie unbeweisbarer Satz über endliche Folgen von natürlichen Zahlen
• Certified Kruskal's Tree Theorem
• Types for Proofs and Programs
• Ordering by Divisibility in Abstract Algebras

This page was built for publication: Higman’s Lemma and Its Computational Content