Edinburgh Research Explorer

IsaPlanner: A Prototype Proof Planner in Isabelle

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

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
Pages279-283
Number of pages5
ISBN (Electronic)978-3-540-45085-6
ISBN (Print)978-3-540-40559-7
DOIs
Publication statusPublished - 2003

Publication series

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

Abstract

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.

ID: 22950166