Guiding proof search in logical frameworks with rippling
Santiago Negrete, Alan Smaill · 1995
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 [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 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. Introduction Our research is concerned with the development of search techniques for Framework Logics. We use Proof Plans [5] as an environment to reason about such techniques. When doing search in Framework Logics we often find that we want to produce connections between hypotheses and conclusions (i.e. identical expressions on both sides of the sequent) to obtain axioms. In order to obtain such complementary expressions, we first look for them...