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.

• Type: Conference
• Year: 2003
• Where: CADE
• Authors: Lucas Dixon, Jacques D. Fleuriot
• Keywords: Automated Reasoning, CADE 2003, Effective Reasoning Technique, Theorem Prover Isabelle