IsaPlanner is a generic framework for proof planning in the interactive theorem prover Isabelle. This is the Wiki, but there is also an IsaPlanner homepage which contains documentation and download links.
We are currently working on version 2 of IsaPlanner which we hope will be released in very soon. We have made significant changes to the underlying representation. This should make it much easier to write techniques as well as improving the existing ones for inductive theorem proving. In particular, we will now support meta-variables for critics and syntehsis, rippling with conditional rule, and-branches during rippling. We plan to illustrate the techniques on properties of trees, lists, natural numbers and ordinal arithmetic.
DownloadInstallSetup - how download, install and setup Isabelle/IsaPlanner
IsaCoSy - synthesis of conjectures
IsaScheme - scheme-based theory exploration
For Developers: The IsaPlanner Cave
DeveloperNews - the latest changes in Subversion
IsabelleDocs - a light to the darker caves of Isabelle
ToDo - things to be done...
RelationalRippling - progress on this project
InductiveProversOfTheWorld - a list of all inductive theorem provers that we know about.
ObservationsAboutSML - things I would like to fix in the language