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


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

For Developers: The IsaPlanner Cave

For Others

alt="The IsaPlanner Cave"

Home (last edited 2010-01-29 18:14:35 by ldixon)