Proof pearl: a formal proof of Higman's lemma in ACL2

DOI10.1007/s10817-010-9178-xzbMath1243.68269OpenAlexW1964096523WikidataQ124838861 ScholiaQ124838861MaRDI QIDQ438550

Jose Antonio Alonso, María José Hidalgo, Francisco Jesús Martín-Mateos, José Luis Ruiz-Reina

Publication date: 31 July 2012

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-010-9178-x

zbMATH Keywords

formal proofsACL2Higman's lemma

Mathematics Subject Classification ID

Related Items (2)

Certified Kruskal’s Tree Theorem ⋮ Higman’s Lemma and Its Computational Content

Uses Software

• ACL2

Cites Work

• Structured theory development for a mechanized logic
• Well quasi-ordered sets
• Ordinal numbers and the Hilbert basis theorem
• Proving termination with multiset orderings
• Term Rewriting and All That
• Theorem Proving in Higher Order Logics
• Types for Proofs and Programs
• Ordering by Divisibility in Abstract Algebras
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Proof pearl: a formal proof of Higman's lemma in ACL2