Model Existence for Higher Order Logic

  • In this paper we provide a semantical meta-theory that will support the development of higher-order calculi for automated theorem proving like the corresponding methodology has in first-order logic. To reach this goal, we establish classes of models that adequately characterize the existing theorem-proving calculi, that is, so that they are sound and complete to these calculi, and a standard methodology of abstract consistency methods (by providing the necessary model existence theorems) needed to analyze completeness of machine-oriented calculi.

Download full text files

Export metadata

  • Export Bibtex
  • Export RIS

Additional Services

Share in Twitter Search Google Scholar
Metadaten
Author:Christoph Benzmüller, Michael Kohlhase
URN (permanent link):urn:nbn:de:hbz:386-kluedo-3887
Serie (Series number):SEKI Report (97,9)
Document Type:Preprint
Language of publication:English
Year of Completion:1997
Year of Publication:1997
Publishing Institute:Technische Universität Kaiserslautern
Tag:automated theorem proving; higher-order calculi
Faculties / Organisational entities:Fachbereich Informatik
DDC-Cassification:004 Datenverarbeitung; Informatik

$Rev: 12793 $