Edinburgh Research Explorer

Higher Order Rippling in IsaPlanner

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Original languageEnglish
Title of host publicationTheorem Proving in Higher Order Logics
Subtitle of host publication17th International Conference, TPHOLs 2004, Park City, Utah, USA, September 14-17, 2004. Proceedings
PublisherSpringer Berlin Heidelberg
Pages83-98
Number of pages16
ISBN (Electronic)978-3-540-30142-4
ISBN (Print)978-3-540-23017-5
DOIs
Publication statusPublished - 2004

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
Volume3223
ISSN (Print)0302-9743

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.

ID: 22950222