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

DOI10.1007/S10817-010-9178-XzbMATH Open1243.68269OpenAlexW1964096523WikidataQ124838861 ScholiaQ124838861MaRDI QIDQ438550FDOQ438550

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

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

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)

Cites Work

• Proving termination with multiset orderings
• Term Rewriting and All That
• Structured theory development for a mechanized logic
• Ordering by Divisibility in Abstract Algebras
• Title not available (Why is that?)
• Well quasi-ordered sets
• A formal proof of Dickson's lemma in ACL2
• Ordinal numbers and the Hilbert basis theorem
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Theorem Proving in Higher Order Logics
• Types for Proofs and Programs

Cited In (5)

• Certified Kruskal’s Tree Theorem
• Theorem Proving in Higher Order Logics
• Higman’s Lemma and Its Computational Content
• Types for Proofs and Programs
• A formal proof of Dickson's lemma in ACL2

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)