Guiding proof search in logical frameworks with rippling

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.