Synthese 133 (1-2):203 - 235 (2002)
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.
|Keywords||Philosophy Philosophy Epistemology Logic Metaphysics Philosophy of Language|
|Categories||categorize this paper)|
References found in this work BETA
No references found.
Citations of this work BETA
CERES in Higher-Order Logic.Stefan Hetzl, Alexander Leitsch & Daniel Weller - 2011 - Annals of Pure and Applied Logic 162 (12):1001-1034.
Combined Reasoning by Automated Cooperation.Christoph Benzmüller, Volker Sorge, Mateja Jamnik & Manfred Kerber - 2008 - Journal of Applied Logic 6 (3):318-342.
Similar books and articles
The Same-Order Monitoring Theory of Consciousness.Uriah Kriegel - 2006 - In Uriah Kriegel & Kenneth Williford (eds.), Self-Representational Approaches to Consciousness. MIT Press. pp. 143--170.
A Mechanization of Sorted Higher-Order Logic Based on the Resolution Principle.Michael Kohlhase - unknown
Higher-Order Semantics and Extensionality.Christoph Benzmüller, Chad E. Brown & Michael Kohlhase - 2004 - Journal of Symbolic Logic 69 (4):1027 - 1088.
Higher-Order Multi-Valued Resolution.Michael Kohlhase - 1999 - Journal of Applied Non-Classical Logics 9 (4):455-477.
Higher Order Unification and the Interpretation of Focus.Stephen G. Pulman - 1997 - Linguistics and Philosophy 20 (1):73-115.
Resolution Calculus for the First Order Linear Logic.Grigori Mints - 1993 - Journal of Logic, Language and Information 2 (1):59-83.
Added to index2009-01-28
Total downloads32 ( #162,501 of 2,178,228 )
Recent downloads (6 months)1 ( #316,624 of 2,178,228 )
How can I increase my downloads?