Cited By
View all- Sternagel C(2013)Certified Kruskal’s Tree TheoremCertified Programs and Proofs10.1007/978-3-319-03545-1_12(178-193)Online publication date: 11-Dec-2013
Proof Pearl: a Formal Proof of Higman's Lemma in ACL2
Authors: 
Francisco Jesús Martín-Mateos, José Luis Ruiz-Reina, José Antonio Alonso, María José HidalgoAuthors Info & Claims
Pages 229 - 250
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.
References
[1]
Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)
[2]
Berghofer, S.: A constructive proof of Higman's lemma in Isabelle. In: Types for Proofs and Programs, TYPES'04, vol. 3085, pp. 66-82. LNCS, Springer, Berlin (2004)
[3]
Coquand, T., Fridlender, D.: A proof of Higman's lemma by structural induction. Unpublished draft, available at http://www.brics.dk/~daniel/texts/open.ps (1993)
[4]
Dershowitz, N., Manna, Z.: Proving termination with multiset orderings. Commun. ACM 22(8), 465-476 (1979)
[5]
Fridlender, D.: Higman's Lemma in Type Theory. Ph.D. thesis, University of Göteborg (1997)
[6]
Herbelin, H.: A program from an A-translated impredicative proof of Higman's Lemma. Available at http://coq.inria.fr/contribs/HigmanNW.html (1994)
[7]
Higman, G.: Ordering by divisibility in abstract algebras. Proc. Lond. Math. Soc. 3(2), 326-336 (1952)
[8]
Kaufmann, M., Manolios, P., Moore, J S.: Computer-Aided Reasoning: An Approach. Kluwer Academic, Boston (2000)
[9]
Kaufmann, M., Moore, J S.: ACL2 Version 3.5, Homepage: http://www.cs.utexas.edu/users/ moore/acl2/ (2009)
[10]
Kaufmann, M., Moore, J S.: Structured theory development for a mechanized logic. J. Autom. Reason. 26(2), 161-203 (2001)
[11]
Martín-Mateos, F.J., Alonso, J.A., Hidalgo, M.J., Ruiz-Reina, J.L.: A formal proof of Dickson's lemma in ACL2. In: Proceedings of LPAR'03, vol. 2850, pp. 49-58. LNAI, Springer, Berlin (2003)
[12]
Martín-Mateos, F.J., Ruiz-Reina, J.L., Alonso, J.A., Hidalgo, M.J.: Proof pearl: a formal proof of Higman's lemma in ACL2. In: Proceedings of TPHOL'05, vol. 3603, pp. 358-372. LNCS, Springer, Berlin (2005)
[13]
Murthy, C.: Extracting Constructive Content from Classical Proofs. Ph.D. thesis, Cornell University (1990)
[14]
Murthy, C., Russell, J.R.: A constructive proof of Higman's lemma. In: Fifth Annual IEEE Symposium on Logic in Computer Science, pp. 257-269 (1990)
[15]
Nash-Williams, C.: On well-quasi-ordering finite trees. Proc. Camb. Philos. Soc. 59(4), 833-835 (1963)
[16]
Richman, F., Stolzenberg, G.: Well quasi-ordered sets. Adv. Math. 97, 145-153 (1993)
[17]
Ruiz-Reina, J.L., Alonso, J.A., Hidalgo, M.J., Martín-Mateos, F.J.: Termination in ACL2 Using Multiset Relations. In: Thirty Five Years of Automating Mathematics, Kluwer Academic, Boston (2003)
[18]
Seisenberger, M.: On the Constructive Content of Proofs, Ph.D. thesis, Fakultät für Mathematik, Ludwig-Maximilians-Universität München (2003)
[19]
Seisenberger, M.: An Inductive Version of Nash-Williams' Minimal-Bad-Sequence Argument for Higman's Lemma. In: Types for Proofs and Programs, TYPES'00, vol. 2277, pp. 233-242. LNCS, Springer, Berlin (2002)
[20]
Simpson, S.G.: Ordinal numbers and the Hilbert basis theorem. J. Symb. Log. 53(3), 961-974 (1988)
Index Terms
- Proof Pearl: a Formal Proof of Higman's Lemma in ACL2
Index terms have been assigned to the content through auto-classification.
Recommendations
Proof pearl: a formal proof of Higman's Lemma in ACL2
TPHOLs'05: Proceedings of the 18th international conference on Theorem Proving in Higher Order LogicsIn this paper we present a formalization and proof of Higman's Lemma in ACL2. We formalize the constructive proof described in [10] where the result is proved using a termination argument justified by the multiset extension of a well-founded relation. ...
Proof Pearl: A Formal Proof of Dally and Seitz' Necessary and Sufficient Condition for Deadlock-Free Routing in Interconnection Networks
Avoiding deadlock is crucial to interconnection networks. In '87, Dally and Seitz proposed a necessary and sufficient condition for deadlock-free routing. This condition states that a routing function is deadlock-free if and only if its channel ...
A Full Formalization of SLD-Resolution in the Calculus of Inductive Constructions
This paper presents a full formalization of the semantics of definite programs, in the calculus of inductive constructions. First, we describe a formalization of the proof of first-order terms unification: this proof is obtained from a similar proof ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Copyright © Copyright © 2011 Springer Science+Business Media B.V.
Publisher
Springer-Verlag
Berlin, Heidelberg
Publication History
Published: 01 October 2011
Author Tags
Qualifiers
- Article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 0Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 22 Sep 2024
Other Metrics
Citations
Cited By
View all- Sternagel C(2013)Certified Kruskal’s Tree TheoremCertified Programs and Proofs10.1007/978-3-319-03545-1_12(178-193)Online publication date: 11-Dec-2013
View Options
View options
Get Access
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in