Comparing approaches to resolution based higher-order theorem proving
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 | ||||||||||
| Options |
|
|||||||||
Download options| PhilPapers Archive |
Upload a copy of this paper Check publisher's policy on self-archival Papers currently archived: 5,679 |
| External links |
 |
| Through your library | Configure |
Similar books and articlesUriah 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.
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.
Analytics
Monthly downloads
Sorry, there are not enough data points to plot this chart.
|
Added to index2009-01-28Total downloads1 ( #274,651 of 549,070 )Recent downloads (6 months)0How can I increase my downloads? |
My notes
Discussion
