Multimodal logic programming using equational and order-sorted logic
type: Item
instance of: scholarly article
title: Multimodal logic programming using equational and order-sorted logic
zbMATH Open document ID: 0756.68090
DOI: 10.1016/0304-3975(92)90290-V
author: Françoise Debart
author: Patrice Enjalbert
author: Madeleine Lescot
published in: Theoretical Computer Science
publication date: 1993-01-16T00:00:00Z
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.
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 68N17
Mathematics Subject Classification ID: 03B35
zbMATH DE Number: 96006
zbMATH Keywords: SLD-E resolution
zbMATH Keywords: modal logic
zbMATH Keywords: unification algorithm
zbMATH Keywords: functional translation
reviewed by: Hans Jürgen Ohlbach
MaRDI profile type: Publication
cites work: Q3998525
cites work: Q3490986
cites work: Modal Theorem Proving: An Equational Viewpoint
cites work: Strategies for modal resolution: Results and problems
cites work: Modal resolution in clausal form
cites work: MOLOG: A system that extends PROLOG with modal logic
cites work: Q4028792
cites work: Q3812209
cites work: Q3030249
cites work: Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations
cites work: Q3773852
cites work: First-order dynamic logic
cites work: Q4012252
cites work: Q3339245
cites work: Q3791114
cites work: Semantics-Based Translation Methods for Modal Logics
cites work: Towards a unified theory of intensional logic programming
cites work: Q5678447
cites work: Q3786020
cites work: Q3992821
description: scientific article; zbMATH DE number 96006