file.pdf (2.86 MB)

A calculus and a system architecture for extensional higher-order resolution

Download (2.86 MB)
journal contribution
posted on 01.01.1997, 00:00 by Christoph Benzmüller
Abstract: "The first part of this paper introduces an extension for a variant of Huet's higher-order resolution calculus [Hue72, Hue73] based upon classical type theory (Church's typed [lambda]-calculus [Chu40]) in order to obtain a calculus which is complete with respect to Henkin models [Hen50]. The new rules connect higher-order pre-unification with the general refutation process in an appropriate way to establish full extensionality for the whole system. The general idea of the calculus is discussed on different examples. The second part introduces the Leo system which implements the discussed extensional higher-order resolution calculus. This part mainly focus [sic] on the embedding of the new extensionality rules into the refutation process and the treatment of higher-order unification."

History

Publisher Statement

All Rights Reserved

Date

01/01/1997

Exports

Exports