Optimization of deduction for Multi-Modal Logics

Abstract

Automated deduction methods facilitate the usage of modal logic in AI. Beside methods, both based on deduction rules for the object language (Fitting, 1983) (Enjalbert Fariñas del Cerro, 1986), there are translation methods that rely on an embedding of the Kripke semantics into first-order logic. Translation methods may carry an advantage in that they are modular, and offer the possibility to re-use the tools, strategies, provers... that have been designed and used for classical logic for about 30 years. Translation methods can be divided into two distinct approaches:

• The relational translation (Moore, 1980): the target logic contains one or more distinguished predicate(s) that simulate the relation(s) in the Kripke semantics. Thus the formula ǹp is translated into (∃W₀∀w)(R(w₀, w)→ p(w)) where w₀ is the initial world and p(w) denotes in the target language that p (propositional variable of the object language) is true at the world w. Of course, this translation preserves satisfiability, and if the relations satisfy some property, reflexivity for example, this must be reflected by a theory in the target logic. As one can see, this translation is a direct simulation of the Kripke semantics. In the predicate case, a modal formula such as ǹp(x) is translated into (∃W₀∀w)(R(w₀, w)→ p(x, w)). With this method, it is necessary to provide a special treatment for the R-predicate(s). (Frisch Scherl, 1991)).