• search hit 2 of 3
Back to Result List

Henkin Completeness of Higher-Order Resolution

  • In this paper we present an extensional higher-order resolution calculus that iscomplete relative to Henkin model semantics. The treatment of the extensionality princi-ples - necessary for the completeness result - by specialized (goal-directed) inference rulesis of practical applicability, as an implentation of the calculus in the Leo-System shows.Furthermore, we prove the long-standing conjecture, that it is sufficient to restrict the orderof primitive substitutions to the order of input formulae.

Download full text files

Export metadata

Additional Services

Share in Twitter Search Google Scholar
Author:Christoph Benzmüller, Michael Kohlhase
URN (permanent link):urn:nbn:de:hbz:386-kluedo-3813
Serie (Series number):SEKI Report (97,10)
Document Type:Preprint
Language of publication:English
Year of Completion:1999
Year of Publication:1999
Publishing Institute:Technische Universität Kaiserslautern
Date of the Publication (Server):2000/04/03
Faculties / Organisational entities:Fachbereich Informatik
DDC-Cassification:0 Allgemeines, Informatik, Informationswissenschaft / 004 Informatik
Licence (German):Standard gemäß KLUEDO-Leitlinien vor dem 27.05.2011