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

IsaPlanner

Proof planning, rippling, and inductive theorem proving for the Isabelle proof assistant

What is IsaPlanner?

IsaPlanner is a generic framework for proof planning in the interactive theorem prover Isabelle. It facilitates the encoding of reasoning techniques, which can be used to conjecture and prove theorems automatically. The system provides an interactive tracing tool that allows you to interact the proof planning attempt. (see the screenshot of IsaPlanner being used with Isabelle and Proof General) It is based on the Isabelle theorem prover and the Isar language. The main proof technique written in IsaPlanner is an inductive theorem prover based on Rippling. This is applicable within Isabelle's Higher Order Logic, and can easily be adapted to Isabelle's other logics.

The system now the main platform for proof planning research in the Edinburgh mathematical reasoning group, and its development is being continued by Lucas Dixon and Moa Johansson in the mathematical reasoning group, at the University of Edinburgh.

IsaPlanner development is hosted on sourceforge under the GNU General Public License (GPL).

For reporting bugs, please use the IsaPlanner trac site.

If you would like to help, become involved in this project, or work in collaboration, please feel free to contact: Lucas Dixon. There is also an IsaPlanner google group/email list to which announcements will be sent and where you are welcome to ask questions and discuss issues relating to proof planning and IsaPlanner.

The IsaPlanner Wiki documents the system, gives information for downloading and setting it up, details development issues, features, and monsters still lurking in the system.

Other Inductive Theorem Provers

The IsaPlanner wiki has a list of the automatic inductive theorem provers, that we know of. Please do let us know any others.

Related Publications

(you can copy/paste from this bibtex file)

IsaPlanner Projects

The following list briefly describes the projects using IsaPlanner that are currently in progress. If you know of any additional projects or would like to start a new one using IsaPlanner, then please let us know by emailing lucas.dixon at ed.ac.uk.

A Framework for Rippling
We have developed a framework for rippling in IsaPlanner that allows easy experimentation with various modification to rippling. This primarily allows experiments with different search strategies and measures. The result is the provision of various rippling tactics for Isabelle. This is a dynamic varient of rippling and supports higher order logics.

An Inductive Theorem Prover
We are using IsaPlanner to provide an inductive theorem proving tactic for Isabelle.

Case Splitting
Experiments with including case-splitting for if- and case-statements within rippling.

Best First Rippling
Experiments with best first search for proof planning in IsaPlanner.

Lemma Discovary
Discovering unknown lemmas and theorems, generalisations, case-splits and other so called eureka steps, are major challenges for automated theorem proving. The project concerns automated discovary of lemmas which has generally been assumed that lemma discovery requires user intervention.

The Generation of Natural Language from IsaPlanner Traces/Proof Plans
Following the MSc project of Marianthi Alexoudi we interested in integrating and extending her work on the generation of natural language proofs from IsaPlanner traces and proof plans.

Hierarchical Proofs
We are developing a system for presenting and manipulating hierarchical proofs generated by proof planning in IsaPlanner. This is written in Java and is in the HiGraph module which can be downloaded form the sourceforge subversion.

Integration of IsaPlanner with Proof General
We are looking into ways to integrate proof planning with interactive theory development and in particular considering how the PGIP protocal can be extended to support such interactions. We will use to provide interactive tools in the latest version of Proof General.

Deductive Synthesis of Induction Schemes
We are interested in extending IsaPlanner to support the automatic derivation of induction schemes duing the process of a deductive synthesis proof. This includes porting the Dynamis system from LambdaClam to IsaPlanner.

Deductive Synthesis of Grid Workflows using Linear Logic
We are developing new machinery to aid the deductive sythesis process in Isabelle and applying this to the synthesis of proof terms for linear logic in order to automatically create grid workflows.

Projects Using IsaPlanner Technology

Isabelle - rewriting using Zippers provides the basis for the substitution tactic of Isabelle. This provides controlled for equational reasoning which can occur under lambda abstractions. This has been used in the L4 verification project and also in EPSRC grants GR/S01771/01, GR/R01156/01, GR/S76328/01, GR/S25388/01, EP/E005713/1, GR/R01156/01, GR/N64571/01, GR/T11715/01, EP/C510712/1, EP/F036345/1, GR/N37414/01.


Quantomatic - A system for reasoning about quantum information; this uses the name-management libraries of IsaPlanner to develop tools for working with graphs that represent compact closed categories and which can be used for symbolic evaluation of quantum processes. EPSRC grants using this include: EP/E045006/1, EP/D072786/1, EP/E005713/1


IsaCoSy - A system developed by Moa Johansson for her PhD project on automated discovery of inductive lemmas, funded by EPSRC grant EP/P501407/1. This uses the inductive theorem prover in IsaPlanner and extends it using lemma-speculation critics as well other other lemma discovary techniques.


IsaScheme - the PhD project of Omar Rivas, investigating schema-based theory formation. This uses IsaPlanner to prove the automatically generated conjectures.


Vanitity Theorem Proving - A spin off-company using IsaPlanner and IsaCoSy to generate new theorems.
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.