Advertisement

LearnΩmatic: System Description

  • Mateja Jamnik
  • Manfred Kerber
  • Martin Pollet
Conference paper
  • 277 Downloads
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2392)

Abstract

We devised a framework within which a proof planning [1] system can learn frequently occurring patterns of reasoning automatically from a number of typical examples, and then use them in proving new theorems [2]. The availability of such patterns, captured as proof methods in a proof planning system, reduces search and proof length. We implemented this learning framework for the proof planner Ωmega [3], and present it in this paper — we call our system LearnΩmatic. The entire process of learning and using new proof methods in LearnΩmatic onsists of the following steps:
  1. 1.

    The user chooses informative examples and gives them to Ωmega to be automatically proved. Traces of these proofs are stored.

     
  2. 2.

    Proof traces of typical examples are given to the learning mechanism which utomatically learns so-called method outlines.

     
  3. 3.

    Method outlines are automatically enriched by adding to them additional information and performing search for information that cannot be reconstructed n order to get fully fleshed proof methods that Ωmega can use in roofs of new theorems.

     

Keywords

Method Outline Residue Class Proof Method Automate Deduction 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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Bundy, A.: The use of explicit plans to guide inductive proofs. In 9th Conference on Automated Deduction. LNCS 310, Springer (1988), 111–120.CrossRefGoogle Scholar
  2. 2.
    Jamnik, M., Kerber, M., Pollet, M., Benzmüller, C.: Automatic learning of proof methods in proof planning. Technical Report CSRP-02-05, School of Computer Science, The University of Birmingham, Birmingham, England, UK, (2002). ftp://ftp.cs.bham.ac.uk/pub/tech-reports/2002/CSRP-02-05.ps.gz Google Scholar
  3. 3.
    Benzmüller, C., et al.: Ωmega: Towards a mathematical assistant. In 14th Conference on Automated Deduction. LNAI 1249, Springer (1997), 252–255.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Mateja Jamnik
    • 1
    • 2
  • Manfred Kerber
    • 2
  • Martin Pollet
    • 2
    • 3
  1. 1.Computer LaboratoryUniversity of CambridgeCambridgeEngland, UK
  2. 2.School of Computer ScienceThe University of BirminghamBirminghamEngland, UK
  3. 3.Fachbereich InformatikUniversität des SaarlandesSaarbrückenGermany

Personalised recommendations