Modern applications of logic in computer science and artificial intelligence often require languages able to represent knowledge about dynamic systems (such as program executions, information flows, distributed and multi-agent systems, temporal databases, etc.).
Extensions of first order predicate logic with program, temporal and other ‘modal’ operators certainly have enough expressive power for this purpose. However, they usually turn out to be highly undecidable. An attractive way to avoid this difficulty is to take as basis not full first order logic but sufficiently expressive fragments of it — for instance, concept description (or terminological) logics that have been developed and used as formalisms for representing and processing knowledge about static application domains.
Our main aim in this project is to find out which parameters of the constituent logics cause undecidability, and to use this knowledge for designing maximally expressive decidable and implementable temporal, dynamic, and epistemic description logics. We plan to develop general mathematical methods for establishing decidability of temporal and dynamic description logics, to estimate the complexity of satisfiability checking in the resulting logics, and to construct implementable satisfiability-checking procedures.