A Summary of the Doctoral Thesis

``Results on Modal Reasoning with Applications to Modal Deductive Databases''

by Nguyen Anh Linh

Deductive databases and logic programming are fields that have gained a great deal of attention due to their usefulness and a wide range of applications. These fields are closely related to each other, they both use classical logic rules to represent mutual dependencies between relations. While logic programming is mostly used in artificial intelligence systems, deductive databases are systems in which the amount of data is much greater than the number of rules. Primarily, logic rules in such systems are restricted to the positive form, i.e. to universally quantified Horn clauses of the classical first-order logic. It is known that with such restriction the least model for a program (or a database) is computable in polynomial time and its size is bounded by a polynomial.

When trying to extend the fields of deductive databases and logic programming to deal with modal logics, a natural attempt is to consider the modal Horn fragment. Unfortunately, it has been shown by Chen and Lin [3] that the problem of checking satisfiability of a set of modal Horn formulae in the propositional modal logics K, KD, T, KB, KDB, B, K4, KD4 and S4 is PSPACE-complete. Due to this fact, modal logic programming has not gained much interest from researchers. Moreover, the modal Horn fragment has been only, as known to us, studied in the context of top-down methods, which are suitable for logic programming but not deductive databases. With bottom-up methods, we often deal with constructing the least models for positive programs. Having the least model of a positive program, all queries for that program can be effectively answered.

Complexity of modal logics has been studied by several authors. In [10] Ladner showed that the complexity of provability in the propositional modal logics K, T, and S4 is PSPACE-complete, and in S5 is co-NP-complete. In [4] Fariñas del Cerro and Penttonen showed that the problem of checking whether a set of modal Horn formulae is satisfiable in S5 is solvable in PTIME. In [3] Chen and Lin showed that the similar problem for a propositional modal logic L which is a normal extension of K5, write $K5 \leq L$, is also solvable in PTIME. Chen and Lin also proved that for a propositional normal modal logic L such that $K \leq L \leq S4$ or $K \leq L \leq B$, the problem is PSPACE-complete. Recently, some authors have analyzed space requirement for propositional modal logics. In [7] Hudelmaier showed that provability for the logic S4 is decidable in $O(n^2.\log{n})$-space, for the logic K in $O(n.\log{n})$-space. In [1,12,2] Basin, Matthews and Viganò showed that provability for the logic KD is decidable in $O(n.\log{n})$-space, and for the logics T, K4 and KD4 in $O(n^2.\log{n})$-space.