Graduate studies at Western
Synthese 133 (1-2):203 - 235 (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(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||No keywords specified (fix it)|
|Categories||categorize this paper)|
|Through your library||Configure|
Similar books and articles
Uriah Kriegel (2006). The Same-Order Monitoring Theory of Consciousness. In Uriah Kriegel & Kenneth Williford (eds.), Self-Representational Approaches to Consciousness. MIT Press.
Stephen G. Pulman (1997). Higher Order Unification and the Interpretation of Focus. Linguistics and Philosophy 20 (1):73-115.
Michael Kohlhase (1999). Higher-Order Multi-Valued Resolution. Journal of Applied Non-Classical Logics 9 (4):455-477.
Christoph Benzmüller, Chad E. Brown & Michael Kohlhase (2004). Higher-Order Semantics and Extensionality. Journal of Symbolic Logic 69 (4):1027 - 1088.
Grigori Mints (1993). Resolution Calculus for the First Order Linear Logic. Journal of Logic, Language and Information 2 (1):59-83.
Sorry, there are not enough data points to plot this chart.
Added to index2009-01-28
Total downloads1 ( #292,381 of 739,344 )
Recent downloads (6 months)0
How can I increase my downloads?