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.

*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]*IsaPlanner 2: A Proof Planner in Isabelle*. L. Dixon and M. Johansson. System Description / Informatics Technical Report 1302. [5 pages, 2007, pdf]*Best-First Rippling*. M. Johansson, A. Bundy and L. Dixon. Strategies in Automated Deduction, part of IJCAR'06. [16 pages, 2006, pdf]*A Proof-Centric approach to Mathematical Assistants*. L. Dixon and J. D. Fleuriot. In Journal of Applied Logic: Special Issue on Mathematics Assistance Systems. [35 pages, 2005, pdf]*A Proof Planning Framework for Isabelle*. L. Dixon. PhD Thesis, Informatics, University of Edinburgh. [225 pages, 2005, pdf]-
*Constructing Induction Rules for Deductive Synthesis Proofs*. A. Bundy, L. Dixon, J. Gow, J. D. Fleuriot. In ENTCS: Constructive Logic for Automated Software Engineering'05. [18 pages, 2005, pdf] *Interactive and Hierarchical Tracing of Techniques in IsaPlanner*. L. Dixon. In ENTCS: User Interfaces for Theorem Provers'05. [13 pages, 2005, pdf].*Higher Order Rippling in IsaPlanner*. L. Dixon and J. D. Fleuriot. Theorem Proving in Higher Order Logics'04, (Springer LNCS Volume 3223, 2004). [16 pages, 2004, 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]

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.

We are using IsaPlanner to provide an inductive theorem proving tactic for Isabelle.

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

Experiments with best first search for proof planning in IsaPlanner.

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.

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.

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

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.

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.