IsaPlanner: A Prototype Proof Planner in Isabelle

Lucas Dixon, Jacques Fleuriot

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract / Description of output

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.
Original languageEnglish
Title of host publicationAutomated Deduction – CADE-19
Subtitle of host publication19th International Conference on Automated Deduction, Miami Beach, FL, USA, July 28 – August 2, 2003. Proceedings
PublisherSpringer Berlin Heidelberg
Number of pages5
ISBN (Electronic)978-3-540-45085-6
ISBN (Print)978-3-540-40559-7
Publication statusPublished - 2003

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
ISSN (Print)0302-9743


Dive into the research topics of 'IsaPlanner: A Prototype Proof Planner in Isabelle'. Together they form a unique fingerprint.

Cite this