IsaPlanner
I am IsaPlanner, a proof planner for Isabelle. I facilitate the encoding of reasoning techniques, which can be used to conjecture and prove theorems automatically. I provide an interactive tracing tool that allows you to interact the proof planning attempt. (see the [http://isaplanner.sourceforge.net/images/isaplanner.png screenshot] of IsaPlanner being used with Isabelle and [http://proofgeneral.inf.ed.ac.uk/ Proof General]) It is based on the [http://www.cl.cam.ac.uk/Research/HVG/Isabelle/ Isabelle] theorem prover and the [http://isabelle.in.tum.de/documentation.html Isar] language. Work is currently in progress on providing a manual for IsaPlanner. If you would like an early draft, or have any questions concerning IsaPlanner, please contact [http://homepages.inf.ed.ac.uk/ldixon/ Lucas Dixon]
