Multi-modal logic programming using equational and order-sorted logic

Abstract

In previous work [2] we proposed a method for automated modal theorem proving based on algebraic concepts and equational techniques. Basically, it uses the translation of Modal Logic into a specially tailored multi-sorted logic called Path Logic. In this paper we extend the method for Multi-Modal logic and apply it to Multi-Modal Logic Programming. The Multi-Modal systems we consider are arbitrary mixing of first order modal systems of type KD,KT,KD4 or KT4, with interaction axioms of the form □_iA - □_jA. Roughly, with each modal subsystem is associated a sort in Path Logic and a specific set of equations, and the interaction axioms are captured by the order relation between sorts. Hence, again, all the modal-logical rules are coded in the unification algorithm. If one considers Horn clauses (in the usual sense) we get a Logic Programming system — PATHLOG- for which standard theoretical results apply. In PATHLOG one can either write programs directly in the language of Path Logic or in various Multi-Modal Logics, the modal formulas being automatically translated and put in clausal form. For instance we obtain as a particular case a system for Temporal Logic Programming which subsumes TEMPLOG of [1], and whose completeness results immediately from our general theorems.

The paper begins with a brief introduction to Multi-Modal Logic. In section 2 we define Path Logic and the translation from Multi-Modal Logic. Section 3 presents PATHLOG and SLD Resolution, illustrated with two examples in section 4. Finally, a comparison with other approaches of Modal Logic Programming is discussed in the conclusion.