Proof pearl: a formal proof of Higman's lemma in ACL2
type: Item
instance of: scholarly article
title: Proof pearl: a formal proof of Higman's lemma in ACL2
zbMATH Open document ID: 1243.68269
author: Francisco Jesús Martín-Mateos
author: José Luis Ruiz-Reina
author: Jose Antonio Alonso
author: María José Hidalgo
published in: Journal of Automated Reasoning
publication date: 2012-07-31T00:00:00Z
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 03E05
Mathematics Subject Classification ID: 05A05
Mathematics Subject Classification ID: 05C85
zbMATH DE Number: 6062053
zbMATH Keywords: Higman's lemma
zbMATH Keywords: formal proofs
zbMATH Keywords: ACL2
describes a project that uses: ACL2
MaRDI profile type: Publication
full work available at URL: s10817-010-9178-x
OpenAlex ID: W1964096523
Wikidata QID: Q124838861
cites work: Term Rewriting and All That
cites work: Types for Proofs and Programs
cites work: Proving termination with multiset orderings
cites work: Q4246946
cites work: Ordering by Divisibility in Abstract Algebras
cites work: Structured theory development for a mechanized logic
cites work: Q3408130
cites work: Theorem Proving in Higher Order Logics
cites work: Q5734436
cites work: Well quasi-ordered sets
cites work: Q4664924
cites work: Q4736401
cites work: Ordinal numbers and the Hilbert basis theorem
DOI: 10.1007/S10817-010-9178-X
description: scientific article; zbMATH DE number 6062053