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
- Scheme-based Theorem Discovery and Concept Invention.
O. Montano-Rivas, R. McCasland, L. Dixon, A. Bundy. (draft of Nov 2010, this is an extended journal version, currently under review for special issue of ESWA, of our MICAI paper, in LNCS 2010) [40
pages, 2010, pdf]
- Conjecture Synthesis for Inductive Theories.
M. Johansson, L. Dixon, A. Bundy. (2010, in JAR) [39
pages, 2010, pdf]
- Lemma Discovery and Middle-Out Reasoning for Automated Inductive Proofs.
M. Johansson, L. Dixon, A. Bundy. (Submitted to conference, currently Informatics Technical Report) [16
pages, 2010, pdf]
- Case-Analysis for Rippling and Inductive Proof.
M. Johansson, L. Dixon, A. Bundy. (Submitted to conference, currently Informatics Technical Report) [16
pages, 2010, pdf]
- IsaCoSy: Synthesis of Inductive Theorems.
M. Johansson, L. Dixon, A. Bundy. Automatheo Workshop 2009 extended abstract [4
pages, 2009, pdf]
- A Proof Planning Framework for Isabelle. L. Dixon. PhD
Thesis, Informatics, University of Edinburgh. [225 pages, 2005, pdf]
- IsaPlanner: A prototype Proof Planner in Isabelle. L. Dixon and J. D. Fleuriot.
19th International Conference on Automated Deduction (CADE'2003),
(Springer LNCS Volume 2741, 2003). [5 pages, 2003, pdf]
(
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.
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.