LearnΩmatic: System Description

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. The user chooses informative examples and gives them to Ωmega to be automatically proved. Traces of these proofs are stored.

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

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