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.
  1. 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
  2. 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.
  3. It was shown that the modal description logics of knowledge and belief are NEXPTIME-complete, while many other constructed logics are NEXPTIME-hard.
  4. 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.
  5. 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.