Proof Pearl: a Formal Proof of Higman’s Lemma in ACL2
Tóm tắt
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.
Tài liệu tham khảo
Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)
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)
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)
Dershowitz, N., Manna, Z.: Proving termination with multiset orderings. Commun. ACM 22(8), 465–476 (1979)
Fridlender, D.: Higman’s Lemma in Type Theory. Ph.D. thesis, University of Göteborg (1997)
Herbelin, H.: A program from an A-translated impredicative proof of Higman’s Lemma. Available at http://coq.inria.fr/contribs/HigmanNW.html (1994)
Higman, G.: Ordering by divisibility in abstract algebras. Proc. Lond. Math. Soc. 3(2), 326–336 (1952)
Kaufmann, M., Manolios, P., Moore, J S.: Computer-Aided Reasoning: An Approach. Kluwer Academic, Boston (2000)
Kaufmann, M., Moore, J S.: ACL2 Version 3.5, Homepage: http://www.cs.utexas.edu/users/moore/acl2/ (2009)
Kaufmann, M., Moore, J S.: Structured theory development for a mechanized logic. J. Autom. Reason. 26(2), 161–203 (2001)
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)
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)
Murthy, C.: Extracting Constructive Content from Classical Proofs. Ph.D. thesis, Cornell University (1990)
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)
Nash-Williams, C.: On well-quasi-ordering finite trees. Proc. Camb. Philos. Soc. 59(4), 833–835 (1963)
Richman, F., Stolzenberg, G.: Well quasi-ordered sets. Adv. Math. 97, 145–153 (1993)
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)
Seisenberger, M.: On the Constructive Content of Proofs, Ph.D. thesis, Fakultät für Mathematik, Ludwig-Maximilians-Universität München (2003)
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)
Simpson, S.G.: Ordinal numbers and the Hilbert basis theorem. J. Symb. Log. 53(3), 961–974 (1988)