Sciweavers

Share
CADE
2003
Springer

IsaPlanner: A Prototype Proof Planner in Isabelle

9 years 6 months ago
IsaPlanner: A Prototype Proof Planner in Isabelle
IsaPlanner is a generic framework for proof planning in the interactive theorem prover Isabelle. It facilitates the encoding of reasoning techniques, which can be used to conjecture and prove theorems automatically. This paper introduces our approach to proof planning, gives and overview of IsaPlanner, and presents one simple yet effective reasoning technique.
Lucas Dixon, Jacques D. Fleuriot
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2003
Where CADE
Authors Lucas Dixon, Jacques D. Fleuriot
Comments (0)
books