|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)|
|Through your library||Only published papers are available at libraries|
Similar books and articles
Robert 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.
Sorry, there are not enough data points to plot this chart.
Added to index2009-01-28
Total downloads2 ( #232,575 of 549,124 )
Recent downloads (6 months)0
How can I increase my downloads?