Repository | Journal | Volume | Articles
(2002) Synthese 133 (1-2).
Comparing approaches to resolution based higher-order theorem proving
Christoph Benzmüller
pp. 203-335
We investigate several approaches to resolution based automated theoremproving in classical higher-order logic (based on Church's simply typedλ-calculus) and discuss their requirements with respect to Henkincompleteness and full extensionality. In particular we focus on Andrews' higher-order resolution (Andrews 1971), Huet's constrained resolution (Huet1972), higher-order E-resolution, and extensional higher-order resolution(Benzmüller and Kohlhase 1997). With the help of examples we illustratethe parallels and differences of the extensionality treatment of these approachesand demonstrate that extensional higher-order resolution is the sole approach thatcan completely avoid additional extensionality axioms.
Publication details
Full citation:
Benzmüller, C. (2002). Comparing approaches to resolution based higher-order theorem proving. Synthese 133 (1-2), pp. 203-335.
This document is unfortunately not available for download at the moment.