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.
The following people are working on the project: