Graduate studies at Western
|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||categorize this paper)|
|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.
Christoph Benzmüller (2002). Comparing Approaches to Resolution Based Higher-Order Theorem Proving. Synthese 133 (1-2):203 - 235.
Christoph Benzmüller, Chad E. Brown & Michael Kohlhase (2004). Higher-Order Semantics and Extensionality. Journal of Symbolic Logic 69 (4):1027 - 1088.
S. Awodey & C. Butz (2000). Topological Completeness for Higher-Order Logic. Journal of Symbolic Logic 65 (3):1168-1182.
Paul E. Griffiths (1989). Folk, Functional and Neurochemical Aspects of Mood. Philosophical Psychology 2 (1):17-32.
Michael Kohlhase (1999). Higher-Order Multi-Valued Resolution. Journal of Applied Non-Classical Logics 9 (4):455-477.
Added to index2009-01-28
Total downloads3 ( #213,731 of 739,344 )
Recent downloads (6 months)1 ( #61,538 of 739,344 )
How can I increase my downloads?