dc.creator | Martín Mateos, Francisco Jesús | es |
dc.creator | Ruiz Reina, José Luis | es |
dc.creator | Alonso Jiménez, José Antonio | es |
dc.creator | Hidalgo Doblado, María José | es |
dc.date.accessioned | 2019-05-13T11:32:30Z | |
dc.date.available | 2019-05-13T11:32:30Z | |
dc.date.issued | 2011 | |
dc.identifier.citation | 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. | |
dc.identifier.issn | 0168-7433 | es |
dc.identifier.uri | https://hdl.handle.net/11441/86293 | |
dc.description.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. | es |
dc.description.sponsorship | Ministerio de Ciencia e Innovación MTM2009-13842-C02-02 | es |
dc.format | application/pdf | es |
dc.language.iso | eng | es |
dc.publisher | Springer | es |
dc.relation.ispartof | Journal of Automated Reasoning, 47 (3), 229-250. | |
dc.rights | Attribution-NonCommercial-NoDerivatives 4.0 Internacional | * |
dc.rights.uri | http://creativecommons.org/licenses/by-nc-nd/4.0/ | * |
dc.subject | Higman’s lemma | es |
dc.subject | Formal proofs | es |
dc.subject | ACL2 | es |
dc.title | Proof Pearl: a Formal Proof of Higman’s Lemma in ACL2 | es |
dc.type | info:eu-repo/semantics/article | es |
dcterms.identifier | https://ror.org/03yxnpp24 | |
dc.type.version | info:eu-repo/semantics/submittedVersion | es |
dc.rights.accessRights | info:eu-repo/semantics/openAccess | es |
dc.contributor.affiliation | Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificial | es |
dc.relation.projectID | MTM2009-13842-C02-02 | es |
dc.relation.publisherversion | https://link.springer.com/article/10.1007/s10817-010-9178-x | es |
dc.identifier.doi | 10.1007/s10817-010-9178-x | es |
dc.contributor.group | Universidad de Sevilla. TIC137: Lógica, Computación e Ingeniería del Conocimiento | es |
idus.format.extent | 22 | es |
dc.journaltitle | Journal of Automated Reasoning | es |
dc.publication.volumen | 47 | es |
dc.publication.issue | 3 | es |
dc.publication.initialPage | 229 | es |
dc.publication.endPage | 250 | es |