A Mechanized Proof of Higman’s Lemma by Open Induction

DOI10.1007/978-3-030-30229-0_12zbMath1446.68188OpenAlexW2998676580MaRDI QIDQ3295156

Christian Sternagel

Publication date: 8 July 2020

Published in: Trends in Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-030-30229-0_12

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Other combinatorial set theory (03E05) Formalization of mathematics in connection with theorem provers (68V20)

Related Items (1)

Dependent choice as a termination principle

Uses Software

• Isabelle/HOL
• CeTA
• Myhill-Nerode
• Well Quasi Orders
• Archive Formal Proofs
• Decreasing Diagrams II
• Open Induction

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Proving open properties by induction
• Isabelle/HOL. A proof assistant for higher-order logic
• Well quasi-ordered sets
• A formalisation of the Myhill-Nerode theorem based on regular expressions
• The theory of well-quasi-ordering: a frequently discovered concept
• 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)
• Certification of Termination Proofs Using CeTA
• Higman’s Lemma and Its Computational Content
• Ramsey's Theorem and the Pigeonhole Principle in Intuitionistic Mathematics
• Certified Kruskal's Tree Theorem
• 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: A Mechanized Proof of Higman’s Lemma by Open Induction