|
Informatics Report Series
|
|
|
|
|
|
|
|
|
| Title:Higher Order Rippling in IsaPlanner |
| Authors:
Lucas Dixon
; Jacques Fleuriot
|
| Date: 2004 |
| Publication Title:in proceedings for conference on Theorem Proving in Higher Order Logics, 2004 |
| Publisher:LNCS |
|
Publication Type:Conference Paper
Publication Status:Published
|
|
Volume No:3223
Page Nos:83-98
|
|
|
- Abstract:
-
We present an account of rippling with proof critics suitable for use in higher order logic in Isabelle/IsaPlanner. We treat issues not previously examined, in particular regarding the existence of multiple annotations during rippling. This results in an efficient mechanism for rippling that can conjecture and prove needed lemmas automatically as well as present the resulting proof plans as Isar style proof scripts.
- Links To Paper
- Personal Copy
- Springer Link
- Bibtex format
- @InProceedings{EDI-INF-RR-0492,
- author = {
Lucas Dixon
and Jacques Fleuriot
},
- title = {Higher Order Rippling in IsaPlanner},
- book title = {in proceedings for conference on Theorem Proving in Higher Order Logics, 2004},
- publisher = {LNCS},
- year = 2004,
- volume = {3223},
- pages = {83-98},
- url = {http://homepages.inf.ed.ac.uk/ldixon/papers/clase-05-dedsynth/clase-05.pdf},
- }
|
