Hilfe Wegweiser Impressum Kontakt Einloggen





First-order modal logic theorem proving and standard PROLOG


Nonnengart,  Andreas
Programming Logics, MPI for Informatics, Max Planck Society;

Externe Ressourcen
Es sind keine Externen Ressourcen verfügbar
Volltexte (frei zugänglich)

(beliebiger Volltext), 198KB

Ergänzendes Material (frei zugänglich)
Es sind keine frei zugänglichen Ergänzenden Materialien verfügbar

Nonnengart, A.(1992). First-order modal logic theorem proving and standard PROLOG (MPI-I-92-228). Saarbrücken: Max-Planck-Institut für Informatik.

Many attempts have been started to combine logic programming and modal logics. Most of them however, do not use classical PROLOG, but extend the PROLOG idea in order to cope with modal logic formulae directly. These approaches have the disadvantage that for each logic new logic programming systems are to be developed and the knowledge and experience gathered from PROLOG can hardly be utilized. Modal logics based on Kripke-style relational semantics, however, allow a direct translation from modal logic into first-order predicate logic by a straightforward translation of the given relational semantics. Unfortunately such a translation turns out to be rather na\"{\i}ve as the size of formulae increases exponentially during the translation. This paper now introduces a translation method which avoids such a representational overhead. Its basic idea relies on the fact that any binary relation can be replaced by equations and inequations which (under certain circumstances) can be eliminated later on by some further transformation. The overall approach thus works essentially for any modal logic having a Kripke-style possible world semantics and first-order describable frame properties. If at all, its application as a pre-processing for PROLOG is limited merely by the possibility of having frame properties which are not Horn or not even first-order describable.