The University of Edinburgh -
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
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.

[Search These Pages] [DAI Home Page] [Comment]