The search result changed since you submitted your search request. Documents might be displayed in a different sort order.
  • search hit 1 of 24
Back to Result List

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

Additional Services

Search Google Scholar
Metadaten
Author:Christoph Benzmüller, Michael Kohlhase
URN:urn:nbn:de:hbz:386-kluedo-3887
Series (Serial Number):SEKI Report (97,9)
Document Type:Preprint
Language of publication:English
Year of Completion:1997
Year of first Publication:1997
Publishing Institution:Technische Universität Kaiserslautern
Date of the Publication (Server):2000/04/03
Tag:automated theorem proving; higher-order calculi
Faculties / Organisational entities:Kaiserslautern - Fachbereich Informatik
DDC-Cassification:0 Allgemeines, Informatik, Informationswissenschaft / 004 Informatik
Licence (German):Standard gemäß KLUEDO-Leitlinien vor dem 27.05.2011