News

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.

For Users

• DownloadInstallSetup - how download, install and setup Isabelle/IsaPlanner

• IsaCoSy - synthesis of conjectures

• IsaScheme - scheme-based theory exploration

• IsaPlannerMethod - how to call IsaPlanner from Isabelle/Isar

For Developers: The IsaPlanner Cave

• DeveloperNews - the latest changes in Subversion

• DeveloperDocs - a guide to adventuring in the catacombs of IsaPlanner

• IsabelleDocs - a light to the darker caves of Isabelle

• HorribleMonsters (bugs) are managed at the IsaPlanner trac web site. (please submit bug reports here)

• ToDo - things to be done...

• The HiGraphInterface

• RelationalRippling - progress on this project

• InductiveProversOfTheWorld - a list of all inductive theorem provers that we know about.

For Others

• ObservationsAboutSML - things I would like to fix in the language