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.

Export metadata

  • Export Bibtex
  • Export RIS

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
Faculties / Organisational entities:Fachbereich Informatik
DDC-Cassification:004 Datenverarbeitung; Informatik

$Rev: 12793 $