The University of Edinburgh -
Division of Informatics
Forrest Hill & 80 South Bridge

Research Paper #750

Title:Guiding Proof Search in Logical Frameworks with Rippling
Authors:Negrete-Yankelevich,S; Smaill,AD
Date:May 1995
Presented:Presented to the workshop In Search in Type Theories, at CADE 12
Abstract:We present a new approach to search guidance for logics presented within a Logical Framework. This approach is based on the idea of rippling, as used in [Bundy et al 93] to guide the search for inductive proofs and, more recently, in some non-inductive domains as well. We present our ideas with respect to the Edinburgh Logical Framework (LF) style of representation of logics but conjecture that our approach could be extended to other Logical Frameworks. We discuss some experiments we have carried out in LF and indicate some possible future research.

[Search These Pages] [DAI Home Page] [Comment]