Skip to main content
SpringerLink
Log in

Overview and Evaluation of Premise Selection Techniques for Large Theory Mathematics

  • Conference paper
Automated Reasoning (IJCAR 2012)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 7364))

Included in the following conference series:

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  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. 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)

    Chapter  Google Scholar 

  3. Bem, J.: The Zermelo proof checker, http://zermelo.org/

  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. 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)

    Chapter  Google Scholar 

  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. 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. 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)

    Chapter  Google Scholar 

  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)

    Article  Google Scholar 

  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. 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)

    Chapter  Google Scholar 

  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. 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)

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Article  Google Scholar 

  16. McCune, W.: Prover9 and Mace4 (2005-2010), http://www.cs.unm.edu/~mccune/prover9/

  17. Meng, J., Paulson, L.C.: Lightweight relevance filtering for machine-generated resolution problems. J. Applied Logic 7(1), 41–57 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

  19. Otten, J., Bibel, W.: leanCoP: lean connection-based theorem proving. J. Symb. Comput. 36(1-2), 139–161 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  20. Polikar, R.: Ensemble based systems in decision making. IEEE Circuits and Systems Magazine 6(3), 21–45 (2006)

    Article  Google Scholar 

  21. Pudlak, P.: Semantic Selection of Premisses for Automated Theorem Proving. In: Sutcliffe et al. [31]

    Google Scholar 

  22. Reichelt, S.: The HLM proof assistant, http://hlm.sourceforge.net/

  23. Riazanov, A., Voronkov, A.: The design and implementation of VAMPIRE. AI Commun. 15(2-3), 91–110 (2002)

    MATH  Google Scholar 

  24. Roederer, A., Puzis, Y., Sutcliffe, G.: Divvy: An ATP Meta-system Based on Axiom Relevance Ordering. In: Schmidt [25], pp. 157–162

    Google Scholar 

  25. Schmidt, R.A. (ed.): CADE-22. LNCS, vol. 5663. Springer, Heidelberg (2009)

    MATH  Google Scholar 

  26. Schulz, S.: Learning search control knowledge for equational deduction. DISKI, vol. 230. Infix Akademische Verlagsgesellschaft (2000)

    Google Scholar 

  27. Schulz, S.: E - A Brainiac Theorem Prover. AI Commun. 15(2-3), 111–126 (2002)

    MATH  Google Scholar 

  28. Sculley, D.: Rank aggregation for similar items. In: SDM. SIAM (2007)

    Google Scholar 

  29. Shawe-Taylor, J., Cristianini, N.: Kernel Methods for Pattern Analysis. Cambridge University Press, New York (2004)

    Book  Google Scholar 

  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)

    Chapter  Google Scholar 

  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. Urban, J.: MizarMode—an integrated proof assistance tool for the Mizar way of formalizing mathematics. Journal of Applied Logic 4(4), 414–427 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  33. Urban, J.: MaLARea: a metasystem for automated reasoning in large theories. In: Sutcliffe et al. [31]

    Google Scholar 

  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. 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)

    Chapter  Google Scholar 

  36. Urban, J., Rudnicki, P., Sutcliffe, G.: ATP and presentation service for Mizar formalizations. CoRR abs/1109.0616 (2011)

    Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  39. Voevodsky, V.: Univalent foundations project (2010) (manuscript), http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations.html

  40. Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: SPASS Version 3.5. In: Schmidt [25], pp. 140–145

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Radboud University, Nijmegen, Netherlands

    Daniel Kühlwein, Twan van Laarhoven, Evgeni Tsivtsivadze, Josef Urban & Tom Heskes

Authors
  1. Daniel Kühlwein
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Twan van Laarhoven
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Evgeni Tsivtsivadze
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Josef Urban
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Tom Heskes
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Fakultät für Informatik, Technische Universität Wien, Favoritenstr. 9, E185/2, 1040, Wien, Austria

    Bernhard Gramlich

  2. École Polytechnique, INRIA Saclay and Laboratoire d’Informatique, Route de Saclay, 91128, Palaiseau Cedex, France

    Dale Miller

  3. School of Computer Science, University of Manchester, Oxford Road, M13 9PL, Manchester, UK

    Uli Sattler

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Kühlwein, D., van Laarhoven, T., Tsivtsivadze, E., Urban, J., Heskes, T. (2012). Overview and Evaluation of Premise Selection Techniques for Large Theory Mathematics. In: Gramlich, B., Miller, D., Sattler, U. (eds) Automated Reasoning. IJCAR 2012. Lecture Notes in Computer Science(), vol 7364. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-31365-3_30

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-31365-3_30

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-31364-6

  • Online ISBN: 978-3-642-31365-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation