LearnΩmatic: System Description
- 277 Downloads
The user chooses informative examples and gives them to Ωmega to be automatically proved. Traces of these proofs are stored.
Proof traces of typical examples are given to the learning mechanism which utomatically learns so-called method outlines.
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.
KeywordsMethod Outline Residue Class Proof Method Automate Deduction Proof Search
Unable to display preview. Download preview PDF.
- 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.Benzmüller, C., et al.: Ωmega: Towards a mathematical assistant. In 14th Conference on Automated Deduction. LNAI 1249, Springer (1997), 252–255.Google Scholar