Multimodal logic programming using equational and order-sorted logic

DOI10.1016/0304-3975(92)90290-VMaRDI QIDQ1199813zbMATH OpenFDO

Authors Françoise Debart, Patrice Enjalbert, Madeleine Lescot

Publication date 16 January 1993

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0304-3975(92)90290-V

zbMATH Keywords

functional translation modal logic SLD-E resolution unification algorithm

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Logic programming (68N17)

Review text

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.

Recommendations

Cites work

Cited in

(19)

This page was built for publication: Multimodal logic programming using equational and order-sorted logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1199813)