System description: { A higher-order theorem prover?
| Abstract | Thus, despite the di culty of higher-order automated theorem proving, which has to deal with problems like the undecidability of higher-order uni - cation (HOU) and the need for primitive substitution, there are proof problems which lie beyond the capabilities of rst-order theorem provers, but instead can be solved easily by an higher-order theorem prover (HOATP) like Leo. This is due to the expressiveness of higher-order Logic and, in the special case of Leo, due to an appropriate handling of the extensionality principles (functional extensionality and extensionality on truth values). | |||||||||
| 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,701 |
| External links |
  Try with proxy. |
| Through your library | Only published papers are available at libraries |
Similar books and articlesRobert Van Gulick (2004). Higher-Order Global States (Hogs): An Alternative Higher-Order Model of Consciousness. In Rocco J. Gennaro (ed.), Higher-Order Theories of Consciousness: An Anthology. John Benjamins.
Paul E. Griffiths (1989). Folk, Functional and Neurochemical Aspects of Mood. Philosophical Psychology 2 (1):17-32.
S. Awodey & C. Butz (2000). Topological Completeness for Higher-Order Logic. Journal of Symbolic Logic 65 (3):1168-1182.
Christoph Benzmüller, Chad E. Brown & Michael Kohlhase (2004). Higher-Order Semantics and Extensionality. Journal of Symbolic Logic 69 (4):1027 - 1088.
Christoph Benzmüller (2002). Comparing Approaches to Resolution Based Higher-Order Theorem Proving. Synthese 133 (1-2):203 - 235.
Analytics
Monthly downloads
Sorry, there are not enough data points to plot this chart.
|
Added to index2009-01-28Total downloads2 ( #232,575 of 549,124 )Recent downloads (6 months)0How can I increase my downloads? |
My notes
Discussion
