sound and complete translations from sorted higher-order logic into sorted first-order logic

  • Extending existing calculi by sorts is astrong means for improving the deductive power offirst-order theorem provers. Since many mathemat-ical facts can be more easily expressed in higher-orderlogic - aside the greater power of higher-order logicin principle - , it is desirable to transfer the advant-ages of sorts in the first-order case to the higher-ordercase. One possible method for automating higher-order logic is the translation of problem formulationsinto first-order logic and the usage of first-order the-orem provers. For a certain class of problems thismethod can compete with proving theorems directlyin higher-order logic as for instance with the TPStheorem prover of Peter Andrews or with the Nuprlproof development environment of Robert Constable.There are translations from unsorted higher-order lo-gic based on Church's simple theory of types intomany-sorted first-order logic, which are sound andcomplete with respect to a Henkin-style general mod-els semantics. In this paper we extend correspond-ing translations to translations of order-sorted higher-order logic into order-sorted first-order logic, thus weare able to utilize corresponding first-order theoremprover for proving higher-order theorems. We do notuse any (lambda)-expressions, therefore we have to add so-called comprehension axioms, which a priori makethe procedure well-suited only for essentially first-order theorems. However, in practical applicationsof mathematics many theorems are essentially first-order and as it seems to be the case, the comprehen-sion axioms can be mastered too.

Metadaten exportieren

  • Export nach Bibtex
  • Export nach RIS

Weitere Dienste

Teilen auf Twitter Suche bei Google Scholar
Verfasserangaben:Manfred Kerber
URN (Permalink):urn:nbn:de:hbz:386-kluedo-2511
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
Fachbereiche / Organisatorische Einheiten:Fachbereich Informatik
DDC-Sachgruppen:0 Allgemeines, Informatik, Informationswissenschaft / 004 Informatik
Lizenz (Deutsch):Standard gemäß KLUEDO-Leitlinien vor dem 27.05.2011

$Rev: 13581 $