Artículo
Proof Pearl: a Formal Proof of Higman’s Lemma in ACL2
Autor/es | Martín Mateos, Francisco Jesús
Ruiz Reina, José Luis Alonso Jiménez, José Antonio Hidalgo Doblado, María José |
Departamento | Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificial |
Fecha de publicación | 2011 |
Fecha de depósito | 2019-05-13 |
Publicado en |
|
Resumen | 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. ... 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. |
Identificador del proyecto | MTM2009-13842-C02-02 |
Cita | 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. |
Ficheros | Tamaño | Formato | Ver | Descripción |
---|---|---|---|---|
Proof Pearl, a Formal Proof of ... | 538.0Kb | [PDF] | Ver/ | |