Informatics Report Series


Report   

EDI-INF-RR-0492


Related Pages

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

Home
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},
}


Home : Publications : Report 

Please mail <reports@inf.ed.ac.uk> with any changes or corrections.
Unless explicitly stated otherwise, all material is copyright The University of Edinburgh