Multimodal logic programming using equational and order-sorted logic (Q1199813)

Modal logics augment predicate logic with the two modal operators \(\square\) (necessarily) and \(\lozenge\) (possibly). By means of these operators, systems with states (``worlds'') can be described very naturally in logic. Multimodal logics have several pairs of these operators. Typical interpretations of a modal formula ``\(\square_ i\Phi\)'' are: ``\(\Phi\) holds always in the future (\(i\) = always-in- future)'', or ``agent \(i\) believes (knows) that \(\Phi\)'' or ``after performing action \(i\), \(\Phi\) holds''. Deduction in modal logic can be done either by means of a special calculus for this logic, or by translating modal formula back into predicate logic and applying predicate logic deduction methods. Some years ago the so called ``functional translation'' has been proposed by several authors. It exploits that binary relations between states (the accessibility relation in Kripke semantics of modal logic) can be represented by a set of functions that map states to accessible states. Semantically this means that sequences of modal operators are translated into strings of terms representing paths through a state graph. These strings of terms become extra arguments of the function and predicate symbols. The particular modal system is represented as an algebraic theory (usually as a set of equations) on these extra terms. In many cases this algebraic theory can be turned into a special theory unification algorithm, and this seems to be the most efficient method for automating deduction in modal logic. The functional translation method is described for the multimodal and quantified version of the systems KD, KT, KD4, KT4 and KF, assuming constant domain semantics. The algebraic description of these theories is turned into a unification algorithm. Furthermore the restriction to modal Horn clauses is considered. This restriction allows a very natural extension of the Prolog like logic programming paradigm to modal logic.