Skip to main content

MaLeCoP Machine Learning Connection Prover

  • Conference paper

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

Abstract

Probabilistic guidance based on learned knowledge is added to the connection tableau calculus and implemented on top of the lean-CoP theorem prover, linking it to an external advisor system. In the typical mathematical setting of solving many problems in a large complex theory, learning from successful solutions is then used for guiding theorem proving attempts in the spirit of the MaLARea system. While in MaLA Rea learning-based axiom selection is done outside unmodified theorem provers, in MaLeCoP the learning-based selection is done inside the prover, and the interaction between learning of knowledge and its application can be much finer. This brings interesting possibilities for further construction and training of self-learning AI mathematical experts on large mathematical libraries, some of which are discussed. The initial implementation is evaluated on the MPTP Challenge large theory benchmark.

Keywords

  • Theorem Prover
  • External System
  • External Advice
  • Large Theory
  • Proof Search

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

This is a preview of subscription content, access via your institution.

Buying options

Chapter
USD   29.95
Price excludes VAT (USA)
  • DOI: 10.1007/978-3-642-22119-4_21
  • Chapter length: 15 pages
  • Instant PDF download
  • Readable on all devices
  • Own it forever
  • Exclusive offer for individuals only
  • Tax calculation will be finalised during checkout
eBook
USD   69.99
Price excludes VAT (USA)
  • ISBN: 978-3-642-22119-4
  • Instant PDF download
  • Readable on all devices
  • Own it forever
  • Exclusive offer for individuals only
  • Tax calculation will be finalised during checkout
Softcover Book
USD   89.99
Price excludes VAT (USA)

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Armando, A., Baumgartner, P., Dowek, G. (eds.): IJCAR 2008. LNCS (LNAI), vol. 5195. Springer, Heidelberg (2008)

    Google Scholar 

  2. Carlson, A., Cumby, C., Rosen, J., Roth, D.: SNoW User’s Guide. Technical Report UIUC-DCS-R-99-210, University of Illinois at Urbana-Champaign (1999)

    Google Scholar 

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

  4. Hoder, K., Voronkov, A.: Sine qua non for large theory reasoning. In: CADE 11 (2011) (To appear)

    Google Scholar 

  5. Meng, J., Paulson, L.C.: Translating higher-order clauses to first-order clauses. J. Autom. Reasoning 40(1), 35–60 (2008)

    MathSciNet  CrossRef  MATH  Google Scholar 

  6. Otten, J., Bibel, W.: leanCoP: Lean Connection-Based Theorem Proving. Journal of Symbolic Computation 36(1-2), 139–161 (2003)

    MathSciNet  CrossRef  MATH  Google Scholar 

  7. Otten, J.: leanCoP 2.0 and ileanCoP 1.2: High performance lean theorem proving in classical and intuitionistic logic (system descriptions). In: Armando, A., et al. (eds.) [1], pp. 283–291

    Google Scholar 

  8. Otten, J.: Restricting backtracking in connection calculi. AI Commun. 23(2-3), 159–182 (2010)

    MathSciNet  MATH  Google Scholar 

  9. Prevosto, V., Waldmann, U.: SPASS+T. In: Sutcliffe, G., Schmidt, R., Schulz, S. (eds.) ESCoR 2006. CEUR, vol. 192, pp. 18–33 (2006)

    Google Scholar 

  10. Riazanov, A., Voronkov, A.: The Design and Implementation of Vampire. AI Communications 15(2-3), 91–110 (2002)

    MATH  Google Scholar 

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

    MATH  Google Scholar 

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

    CrossRef  MATH  Google Scholar 

  13. Suda, M., Sutcliffe, G., Wischnewski, P., Lamotte-Schubert, M., de Melo, G.: External Sources of Axioms in Automated Theorem Proving. In: Mertsching, B., Hund, M., Aziz, Z. (eds.) KI 2009. LNCS, vol. 5803, pp. 281–288. Springer, Heidelberg (2009)

    CrossRef  Google Scholar 

  14. Tsivtsivadze, E., Urban, J., Geuvers, H., Heskes, T.: Semantic graph kernels for automated reasoning. In: SDM 2011 (to appear, 2011)

    Google Scholar 

  15. Urban, J.: MoMM - fast interreduction and retrieval in large libraries of formalized mathematics. International Journal on Artificial Intelligence Tools 15(1), 109–130 (2006)

    CrossRef  Google Scholar 

  16. Urban, J.: MPTP 0.2: Design, implementation, and initial experiments. J. Autom. Reasoning 37(1-2), 21–43 (2006)

    CrossRef  MATH  Google Scholar 

  17. Urban, J., Hoder, K., Voronkov, A.: Evaluation of automated theorem proving on the Mizar Mathematical Library. In: ICMS, pp. 155–166 (2010)

    Google Scholar 

  18. Urban, J., Sutcliffe, G., Pudlák, P., Vyskočil, J.: MaLARea SG1- machine learner for automated reasoning with semantic guidance. In: Armando, et al. (eds.) [1], pp. 441–456

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Editors and Affiliations

Rights and permissions

Reprints and Permissions

Copyright information

© 2011 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Urban, J., Vyskočil, J., Štěpánek, P. (2011). MaLeCoP Machine Learning Connection Prover. In: Brünnler, K., Metcalfe, G. (eds) Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 2011. Lecture Notes in Computer Science(), vol 6793. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-22119-4_21

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-22119-4_21

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-22118-7

  • Online ISBN: 978-3-642-22119-4

  • eBook Packages: Computer ScienceComputer Science (R0)