## 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.

Author: Christoph Benzmüller, Michael Kohlhase urn:nbn:de:hbz:386-kluedo-3887 SEKI Report (97,9) Preprint English 1997 1997 Technische Universität Kaiserslautern automated theorem proving; higher-order calculi Fachbereich Informatik 004 Datenverarbeitung; Informatik

$Rev: 12793$