MRG home page · Research · Publications · Projects · Software · People

Automated Discovery of Inductive Lemmas

Project Description [This project is finished]

Discovering unknown lemmas and theorems, generalisations, case-splits and other so called eureka steps, are major challenges for automated theorem proving. It has generally been assumed that lemma discovery requires user intervention. Consequently, most theorem provers rely on the user to supply any additional lemmas that might be needed. Interactive theorem provers, such as Isabelle, often come with large theory libraries of previously proved lemmas and theorems that are carefully configured and expected to be useful in future proofs. Automating this theory formation process is another important challenge. Given a set of initial definitions, one wish to automatically produce a useful set of theorems about them.

The areas of lemma discovery and theory formation are related. For a powerful theorem prover, with sophisticated techniques for finding lemmas, it may suffice with a simple background theory. However, a richer background theory makes it possible to find many harder proofs more efficiently, without lemma discovery techniques.

We have implemented and evaluated two different approaches for improving automation of higher-order inductive proofs in the IsaPlanner system. Firstly, we have implemented a lemma speculation critic, which attempts to find a missing lemma using information from a failed inductive proof attempt. Lemma speculation has limitations, which led to the implementation of a program for theory formation for inductive theories, which synthesises theorems from recursive datatype- and function definitions. An automated technique for case-analysis has also been implemented, enabling IsaPlanner to deal with proofs involving conditional statements.

Publications

Results

People

The following people are working on the project:

Links

Funding

The project is funded by EPSRC.


Webpage maintained by Moa Johansson
Mathematical Reasoning Group, Informatics Forum, 10 Crichton Street, Edinburgh, EH8 9AB, Scotland
Tel: +44 (0)131 650 2733      Fax: +44 (0)131 650 6899
Please send corrections and suggestions for this page to the DReaM Support Team
Unless explicitly stated otherwise all material on this web site is copyright © The University of Edinburgh.