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 |
| Keywords: | |
| 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. |
| Download: | NO ONLINE COPY |
![[Search These Pages]](http://www.dai.ed.ac.uk/icons/dai_search.gif){kind=icon}
![[DAI Home Page]](http://www.dai.ed.ac.uk/icons/dai_home.gif){kind=icon}
![[Comment]](http://www.dai.ed.ac.uk/icons/dai_comment.gif){kind=icon}