How to Prove Higher Order Theorems in First Order Logic

  • In this paper we are interested in using a firstorder theorem prover to prove theorems thatare formulated in some higher order logic. Tothis end we present translations of higher or-der logics into first order logic with flat sortsand equality and give a sufficient criterion forthe soundness of these translations. In addi-tion translations are introduced that are soundand complete with respect to L. Henkin's gen-eral model semantics. Our higher order logicsare based on a restricted type structure in thesense of A. Church, they have typed functionsymbols and predicate symbols, but no sorts.

Metadaten exportieren

  • Export nach Bibtex
  • Export nach RIS

Weitere Dienste

Teilen auf Twitter Suche bei Google Scholar
Metadaten
Verfasserangaben:Manfred Kerber
URN (Permalink):urn:nbn:de:hbz:386-kluedo-3353
Schriftenreihe (Bandnummer):SEKI Report (90,19)
Dokumentart:Wissenschaftlicher Artikel
Sprache der Veröffentlichung:Englisch
Jahr der Fertigstellung:1999
Jahr der Veröffentlichung:1999
Veröffentlichende Institution:Technische Universität Kaiserslautern
Datum der Publikation (Server):03.04.2000
Freies Schlagwort / Tag:completeness; higher order logic ; morphism ; second order logic ; soundness ; translation
Fachbereiche / Organisatorische Einheiten:Fachbereich Informatik
DDC-Sachgruppen:0 Informatik, Informationswissenschaft, allgemeine Werke / 00 Informatik, Wissen, Systeme / 004 Datenverarbeitung; Informatik
Lizenz (Deutsch):Standard gemäß KLUEDO-Leitlinien vor dem 27.05.2011

$Rev: 13581 $