First-Order Modal Logic Theorem Proving and Functional Simulation
Andreas Nonnengart
FILES: IJCAI93.*
We propose a translation approach from modal logicsto first-order predicate logic which combines advantages from both, the (standard) relational translation and the (rather compact) functional translation method and avoids many of their respective disadvantages (exponential growth versus equality handling). In particular in the application to serial modal logics it allows considerable simplifications such that often even a simple unit clause suffices in order to express the accessibility relation properties. Although we restrict the approach here to first-order modal logic theorem proving it has been shown to be of wider interest, as e.g.\ sorted logic or terminological logic.
Available: DVI BibTeX-Entry
FILES: AI93.*
Standard knowledge representation systems are supposed to be able to represent either common or individual knowledge about the world. In this paper we propose an extension to such knowledge representation systems which, in a uniform manner, allows to express beliefs of multiple agents as well as knowledge, desire, time and in fact any modality which has a first-order predicate logic possible world semantics.
Available: DVI BibTeX-Entry
Home page of the Max Planck Institute
Person responsible for this page