Informatics Report Series



Related Pages

Report (by Number) Index
Report (by Date) Index
Author Index
Institute Index

Title:IsaPlanner: A Prototype Proof Planner in Isabelle
Authors: Lucas Dixon ; Jacques Fleuriot
Date:Jul 2003
Publication Title:Proceedings of CADE 2003 (Conference on Automated Deduction)
Publication Type:Conference Paper Publication Status:Published
Volume No:2741 Page Nos:279-283
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.
Links To Paper
Personal Page
Bibtex format
author = { Lucas Dixon and Jacques Fleuriot },
title = {IsaPlanner: A Prototype Proof Planner in Isabelle},
book title = {Proceedings of CADE 2003 (Conference on Automated Deduction)},
publisher = {Springer},
year = 2003,
month = {Jul},
volume = {2741},
pages = {279-283},
doi = {10.1007/b11829},
url = {},

Home : Publications : Report 

Please mail <> with any changes or corrections.
Unless explicitly stated otherwise, all material is copyright The University of Edinburgh