Division of Informatics
Forrest Hill & 80 South Bridge
Research Paper #799 | |
|---|---|
| Title: | Higher-Order Annotated Terms for Proof Search |
| Authors: | Smaill,AD; Green,I |
| Date: | Mar 1996 |
| Presented: | To appear in the proceedings of the 1996 conference - Theorem Proving in Higher-order Logiscs |
| Keywords: | |
| Abstract: | A notion of embedding appropriate to higher-order syntax is described. This provides a representation of annoted formulae in terms of the difference between pairs of formulae. We define substitution and unification for such annotated terms. Using this representation of annotated terms, the proof search guidance techniques of rippling can be extended to higher-order theorems. We illustrate this by several examples based on an implementation of these in lambda Prolog. |
| 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}