Overview and Evaluation of Premise Selection Techniques for Large Theory Mathematics

  • Daniel Kühlwein
  • Twan van Laarhoven
  • Evgeni Tsivtsivadze
  • Josef Urban
  • Tom Heskes
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7364)

Abstract

In this paper, an overview of state-of-the-art techniques for premise selection in large theory mathematics is provided, and new premise selection techniques are introduced. Several evaluation metrics are introduced, compared and their appropriateness is discussed in the context of automated reasoning in large theory mathematics. The methods are evaluated on the MPTP2078 benchmark, a subset of the Mizar library, and a 10% improvement is obtained over the best method so far.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Alama, J., Heskes, T., Kühlwein, D., Tsivtsivadze, E., Urban, J.: Premise Selection for Mathematics by Corpus Analysis and Kernel Methods. CoRR abs/1108.3446 (2011)Google Scholar
  2. 2.
    Alama, J., Kühlwein, D., Urban, J.: Automated and Human Proofs in General Mathematics: An Initial Comparison. In: Bjørner, N., Voronkov, A. (eds.) LPAR-18 2012. LNCS, vol. 7180, pp. 37–45. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  3. 3.
    Bem, J.: The Zermelo proof checker, http://zermelo.org/
  4. 4.
    Bingham, E., Mannila, H.: Random projection in dimensionality reduction: applications to image and text data. In: KDD, pp. 245–250 (2001)Google Scholar
  5. 5.
    Blanchette, J.C., Bulwahn, L., Nipkow, T.: Automatic Proof and Disproof in Isabelle/HOL. In: Tinelli, C., Sofronie-Stokkermans, V. (eds.) FroCos 2011. LNCS, vol. 6989, pp. 12–27. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  6. 6.
    Carlson, A., Cumby, C., Rosen, J., Roth, D.: The SNoW Learning Architecture. Tech. Rep. UIUCDCS-R-99-2101, UIUC Computer Science Department (May 1999), http://cogcomp.cs.illinois.edu/papers/CCRR99.pdf
  7. 7.
    Chu, W., Park, S.T.: Personalized recommendation on dynamic content using predictive bilinear models. In: Quemada, J., León, G., Maarek, Y.S., Nejdl, W. (eds.) WWW, pp. 691–700. ACM (2009)Google Scholar
  8. 8.
    Cramer, M., Fisseni, B., Koepke, P., Kühlwein, D., Schröder, B., Veldman, J.: The Naproche Project Controlled Natural Language Proof Checking of Mathematical Texts. In: Fuchs, N.E. (ed.) CNL 2009. LNCS, vol. 5972, pp. 170–186. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  9. 9.
    Deerwester, S.C., Dumais, S.T., Landauer, T.K., Furnas, G.W., Harshman, R.A.: Indexing by Latent Semantic Analysis. JASIS 41(6), 391–407 (1990)CrossRefGoogle Scholar
  10. 10.
    Denzinger, J., Fuchs, M., Goller, C., Schulz, S.: Learning from Previous Proof Experience. Technical Report AR99-4, Institut für Informatik, Technische Universität München (1999)Google Scholar
  11. 11.
    Gonthier, G.: Advances in the Formalization of the Odd Order Theorem. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol. 6898, p. 2. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  12. 12.
    Hales, T.C.: Mathematics in the age of the Turing machine. Lecture Notes in Logic (to appear, 2012), http://www.math.pitt.edu/~thales/papers/turing.pdf
  13. 13.
    Hales, T.C., Harrison, J., McLaughlin, S., Nipkow, T., Obua, S., Zumkeller, R.: A revision of the proof of the Kepler Conjecture. Discrete & Computational Geometry 44(1), 1–34 (2010)MathSciNetMATHCrossRefGoogle Scholar
  14. 14.
    Hoder, K., Voronkov, A.: Sine Qua Non for Large Theory Reasoning. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol. 6803, pp. 299–314. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  15. 15.
    Klein, G., Andronick, J., Elphinstone, K., Heiser, G., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: seL4: formal verification of an operating-system kernel. Commun. ACM 53(6), 107–115 (2010)CrossRefGoogle Scholar
  16. 16.
    McCune, W.: Prover9 and Mace4 (2005-2010), http://www.cs.unm.edu/~mccune/prover9/
  17. 17.
    Meng, J., Paulson, L.C.: Lightweight relevance filtering for machine-generated resolution problems. J. Applied Logic 7(1), 41–57 (2009)MathSciNetMATHCrossRefGoogle Scholar
  18. 18.
    de Moura, L., Bjørner, N.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  19. 19.
    Otten, J., Bibel, W.: leanCoP: lean connection-based theorem proving. J. Symb. Comput. 36(1-2), 139–161 (2003)MathSciNetMATHCrossRefGoogle Scholar
  20. 20.
    Polikar, R.: Ensemble based systems in decision making. IEEE Circuits and Systems Magazine 6(3), 21–45 (2006)CrossRefGoogle Scholar
  21. 21.
    Pudlak, P.: Semantic Selection of Premisses for Automated Theorem Proving. In: Sutcliffe et al. [31]Google Scholar
  22. 22.
    Reichelt, S.: The HLM proof assistant, http://hlm.sourceforge.net/
  23. 23.
    Riazanov, A., Voronkov, A.: The design and implementation of VAMPIRE. AI Commun. 15(2-3), 91–110 (2002)MATHGoogle Scholar
  24. 24.
    Roederer, A., Puzis, Y., Sutcliffe, G.: Divvy: An ATP Meta-system Based on Axiom Relevance Ordering. In: Schmidt [25], pp. 157–162Google Scholar
  25. 25.
    Schmidt, R.A. (ed.): CADE-22. LNCS, vol. 5663. Springer, Heidelberg (2009)MATHGoogle Scholar
  26. 26.
    Schulz, S.: Learning search control knowledge for equational deduction. DISKI, vol. 230. Infix Akademische Verlagsgesellschaft (2000)Google Scholar
  27. 27.
    Schulz, S.: E - A Brainiac Theorem Prover. AI Commun. 15(2-3), 111–126 (2002)MATHGoogle Scholar
  28. 28.
    Sculley, D.: Rank aggregation for similar items. In: SDM. SIAM (2007)Google Scholar
  29. 29.
    Shawe-Taylor, J., Cristianini, N.: Kernel Methods for Pattern Analysis. Cambridge University Press, New York (2004)CrossRefGoogle Scholar
  30. 30.
    Sutcliffe, G., Puzis, Y.: SRASS - A Semantic Relevance Axiom Selection System. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 295–310. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  31. 31.
    Sutcliffe, G., Urban, J., Schulz, S. (eds.): Proceedings of the CADE-21 Workshop on Empirically Successful Automated Reasoning in Large Theories, Bremen, Germany, July 17. CEUR Workshop Proceedings, vol. 257. CEUR-WS.org (2007)Google Scholar
  32. 32.
    Urban, J.: MizarMode—an integrated proof assistance tool for the Mizar way of formalizing mathematics. Journal of Applied Logic 4(4), 414–427 (2006)MathSciNetMATHCrossRefGoogle Scholar
  33. 33.
    Urban, J.: MaLARea: a metasystem for automated reasoning in large theories. In: Sutcliffe et al. [31]Google Scholar
  34. 34.
    Urban, J.: An Overview of Methods for Large-Theory Automated Theorem Proving (Invited Paper). In: Höfner, P., McIver, A., Struth, G. (eds.) ATE Workshop. CEUR Workshop Proceedings, vol. 760, pp. 3–8. CEUR-WS.org (2011)Google Scholar
  35. 35.
    Urban, J., Hoder, K., Voronkov, A.: Evaluation of Automated Theorem Proving on the Mizar Mathematical Library. In: Fukuda, K., van der Hoeven, J., Joswig, M., Takayama, N. (eds.) ICMS 2010. LNCS, vol. 6327, pp. 155–166. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  36. 36.
    Urban, J., Rudnicki, P., Sutcliffe, G.: ATP and presentation service for Mizar formalizations. CoRR abs/1109.0616 (2011)Google Scholar
  37. 37.
    Urban, J., Sutcliffe, G., Pudlák, P., Vyskočil, J.: MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 441–456. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  38. 38.
    Urban, J., Vyskočil, J., Štěpánek, P.: MaLeCoP Machine Learning Connection Prover. In: Brünnler, K., Metcalfe, G. (eds.) TABLEAUX 2011. LNCS, vol. 6793, pp. 263–277. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  39. 39.
    Voevodsky, V.: Univalent foundations project (2010) (manuscript), http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations.html
  40. 40.
    Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: SPASS Version 3.5. In: Schmidt [25], pp. 140–145Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2012

Authors and Affiliations

  • Daniel Kühlwein
    • 1
  • Twan van Laarhoven
    • 1
  • Evgeni Tsivtsivadze
    • 1
  • Josef Urban
    • 1
  • Tom Heskes
    • 1
  1. 1.Radboud UniversityNijmegenNetherlands

Personalised recommendations