Report on EPSRC Visiting Fellowship GR/M36748
Fellow: Dr M Zakharyaschev
Title: Temporal and Dynamic Description Logics
The aim of the project was to use mathematical methods of modal logic for
developing and investigating concept description logics intended for knowledge
representation and reasoning in dynamic application domains. In particular,
we wanted to find out which parameters of description logics with modal
operators cause undecidability, and to use this knowledge for designing
maximally expressive and decidable temporal, dynamic, and epistemic description
logics.
The main results of the project are as follows.
-
We developed a new mosaic-type technique for proving decidability of the
satisfiability problem for description logics with various kinds of modal
operators, intended for representing dynamic and intensional knowledge.
This technique was used to
-
construct decidable hybrids of propositional dynamic logic PDL and (decidable)
concept description logics in which the modal operators of PDL can be applied
to concepts (unary predicates) and formulas;
-
construct decidable modal description logics (based on the standard description
language ALC which allow applications of modal operators to all kinds of
syntactic terms---concepts, roles (binary predicates) and formulas---as
well as both local (i.e., state-dependent) and global (i.e., state-independent)
concepts, roles and objects. Satisfiability checking algorithms were constructed
for
-
arbitrary multimodal frames,
-
frames with universal accessibility relations (used for modelling knowledge),
-
frames with transitive, symmetric and euclidean relations (used for modelling
beliefs).
On the other hand, we proved that in the latter case the satisfiability
problem becomes undecidable if the underlying frames are arbitrary strict
linear orders, (N,<) (representing time), or the language contains the
common knowledge operator for at least two agents.
-
It was shown that the modal description logics of knowledge and belief
are NEXPTIME-complete, while many other constructed logics are NEXPTIME-hard.
-
We studied two-dimensional Cartesian products of modal logics determined
by infinite or arbitrarily long finite linear orders, and proved a general
theorem showing that practically always these products turn out to be undecidable.
This theorem solves a number of open problems of Gabbay and Shehtman (1998).
We also established a sufficient condition for such products to be non-recursively
enumerable, and gave a simple axiomatization for the Cartesian square of
the minimal linear logic, using non-structural Gabbay-type inference rules.
-
The developed technique for proving decidability of multi-dimensional propositional
logics was also used for attacking the classical decision problem for first-order
temporal and modal logics. Namely, we introduced a new fragment of the
first-order temporal and modal languages, called the monodic fragment,
in which all formulas beginning with a temporal (or modal) operator have
at most one free variable, and showed that the satisfiability problem for
such formulas in various linear time structures and various modal frames
can be reduced to the satisfiability problem for a certain fragment of
classical first-order logic. This reduction made it possible to single
out a number of decidable fragments of first-order temporal and modal logics,
of two-sorted first-order logics in which one sort is intended for temporal
reasoning, as well as to construct decidable description logics with the
operators Since and Until based on various time-structures. Actually, these
are the first positive decidability results concerning the classical decision
problem for first-order intensional logics.
Contact: Dr I. Hodkinson,
Department of Computing,
Imperial College,
180 Queen's Gate,
London SW7 2BZ, UK.