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

DOI10.1007/S10817-010-9178-XMaRDI QIDQ438550zbMATH OpenOpenAlexWikidataFDO

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

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

ACL2formal proofsHigman's lemma

Mathematics Subject Classification ID

Permutations, words, matrices (05A05) Graph algorithms (graph-theoretic aspects) (05C85) Mechanization of proofs and logical operations (03B35) Other combinatorial set theory (03E05)

Recommendations

• Theorem Proving in Higher Order Logics
• Higman's lemma and its computational content
• Types for Proofs and Programs
• scientific article; zbMATH DE number 1301733
• Certified Kruskal's tree theorem

Cites work

• scientific article; zbMATH DE number 1301733 (Why is no real title available?)
• scientific article; zbMATH DE number 2154398 (Why is no real title available?)
• scientific article; zbMATH DE number 2085177 (Why is no real title available?)
• scientific article; zbMATH DE number 3198033 (Why is no real title available?)
• A formal proof of Dickson's lemma in ACL2
• Ordering by Divisibility in Abstract Algebras
• Ordinal numbers and the Hilbert basis theorem
• Proving termination with multiset orderings
• Structured theory development for a mechanized logic
• Term Rewriting and All That
• Theorem Proving in Higher Order Logics
• Types for Proofs and Programs
• Well quasi-ordered sets

Cited in

(5)

• Higman's lemma and its computational content
• Certified Kruskal's tree theorem
• Theorem Proving in Higher Order Logics
• Types for Proofs and Programs
• A formal proof of Dickson's lemma in ACL2

Describes a project that uses

Uses Software

• ACL2

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q438550)