Guiding proof search in logical frameworks with rippling

Santiago Negrete, Alan Smaill

Research output: Book/ReportOther report


We present a new approach to search guidance for logics presented with a Logical Framework. This approach is based on the idea of rippling, as used in [4] 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 Frameowrk (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.
Original languageEnglish
PublisherUniversity of Edinburgh
Number of pages9
Publication statusPublished - 1995


Dive into the research topics of 'Guiding proof search in logical frameworks with rippling'. Together they form a unique fingerprint.

Cite this