Repositorio de producción científica de la Universidad de Sevilla

Proof Pearl: a Formal Proof of Higman’s Lemma in ACL2

 

Advanced Search
 
Opened Access Proof Pearl: a Formal Proof of Higman’s Lemma in ACL2
Cites

Show item statistics
Icon
Export to
Author: Martín Mateos, Francisco Jesús
Ruiz Reina, José Luis
Alonso Jiménez, José Antonio
Hidalgo Doblado, María José
Department: Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificial
Date: 2011
Published in: Journal of Automated Reasoning, 47 (3), 229-250.
Document type: Article
Abstract: Higman’s lemma is an important result in infinitary combinatorics, which has been formalized in several theorem provers. In this paper we present a formalization and proof of Higman’s Lemma in the ACL2 theorem prover. Our formalization is based on a proof by Murthy and Russell, where the key termination argument is justified by the multiset relation induced by a well-founded relation. To our knowledge, this is the first mechanization of this proof.
Cite: Martín Mateos, F.J., Ruiz Reina, J.L., Alonso Jiménez, J.A. y Hidalgo Doblado, M.J. (2011). Proof Pearl: a Formal Proof of Higman’s Lemma in ACL2. Journal of Automated Reasoning, 47 (3), 229-250.
Size: 538.0Kb
Format: PDF

URI: https://hdl.handle.net/11441/86293

DOI: 10.1007/s10817-010-9178-x

See editor´s version

This work is under a Creative Commons License: 
Attribution-NonCommercial-NoDerivatives 4.0 Internacional

This item appears in the following Collection(s)