Informatics Report Series



Related Pages

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

Title:IsaPlanner 2: A Proof Planner in Isabelle
Authors: Lucas Dixon ; Moa Johansson
Date: 2007
Publication Title:DReaM Technical Report (System description)
Publication Type:Other
We describe version 2 of IsaPlanner, a proof planner for the Isabelle proof assistant and present the central design decisions and their motivations. The major advances are the support for a declarative pre- sentation of the proof plans, reasoning with meta-variables to support middle-out reasoning, new proof critics for lemma speculation and case analysis, the ability to mix search strategies, and the inclusion of a higher-order version of rippling that can use best-first search. The result is a more flexible and powerful proof planner for exploring proof automation in Isabelle.
Links To Paper
1st Link
Bibtex format
author = { Lucas Dixon and Moa Johansson },
title = {IsaPlanner 2: A Proof Planner in Isabelle},
year = 2007,
url = {},
note = {DReaM Technical Report (System description)},

Home : Publications : Report 

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