publication . Article . 2002

COMPARING APPROACHES TO RESOLUTION BASED HIGHER-ORDER THEOREM PROVING

Christoph Benzmüller;
Restricted
  • Published: 01 Jan 2002
Abstract
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(Benzmuller 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 comp...
Subjects
free text keywords: Extensionality, Philosophy of language, Axiom, Automated theorem proving, Extensional definition, Classical logic, Calculus, Mathematics, Completeness (statistics), Second-order logic
Related Organizations
Download fromView all 2 versions
Synthese
Article . 2003
Provider: Crossref
Any information missing or wrong?Report an Issue