- Abstract:
- 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
- @Misc{EDI-INF-RR-1302,
- author = {
Lucas Dixon
and Moa Johansson
},
- title = {IsaPlanner 2: A Proof Planner in Isabelle},
- year = 2007,
- url = {http://dream.inf.ed.ac.uk/projects/isaplanner/docs/isaplanner-v2-07.pdf},
- note = {DReaM Technical Report (System description)},
- }
|
