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. © Springer-Verlag 2004.
Cite
CITATION STYLE
Dixon, L., & Fleuriot, J. (2004). Higher Order Rippling in ISAPLANNER. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 3223, 83–98. https://doi.org/10.1007/978-3-540-30142-4_7
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
