Results

Our main contributions are the following:

• clausal tableau systems and improved decision procedures for the propositional modal logics K, KD, T, KB, KDB, B, K4, KD4, and S4 (see Chapter 3);

• establishment of the best currently known upper space bound $O(n.\log{n})$ for the propositional modal logics K4, KD4, and S4, and O(n²) for KB, KDB, and B (see Section 3.7 and Theorems 3.7.2, 3.7.6, and 3.7.9);

• a new proof for the results of other authors [8,1] such that the propositional modal logics K and KD are decidable in $O(n.\log{n})$-space (see Section 3.7.1 and Theorem 3.7.2);

• the formulation of positive propositional modal logic programs and MDatalog programs (see Definitions 2.4.2 and 5.2.1);

• algorithms of constructing the least models for positive propositional modal logic programs and MDatalog programs in the modal logics KD, T, KDB, B, KD5, KD45, S5, KD4, and S4 (see Algorithms 4.2.1, 4.4.1, and 5.5.1), and conditions that guarantee the algorithms terminating in polynomial time (see Theorems 4.2.6 and 4.4.9, and Corollary 5.4.5);

• a characterization of positive modal logic programs and MDatalog programs in KB, K5, K45, and KB5 by one or two models, which can be effectively constructed (see Section 4.3 and Corollaries 4.3.5 and 5.4.7);

• a theorem showing PTIME complexity of computing queries for a given MDatalog program in the logics KD, T, KB, KDB, B, K5, KD5, K45, KD45, KB5, and S5, provided that the quantifier depths of queries and the program are finitely bounded, and that the modal depth of the program is finitely bounded in the case when the considered logic is not a normal extension of K5 (see Theorem 5.4.8);

• a theorem stating that the problem of checking satisfiability of a set of Horn formulae with finitely bounded modal depths in the propositional modal logics KD, T, KB, KDB, and B is decidable in PTIME (see Corollaries 4.2.7 and 4.3.6);

• a new proof for the results of other authors [4,3] such that the problem of checking satisfiability of a set of Horn formulae in the propositional modal logics K5, KD5, K45, KD45, KB5, and S5 is decidable in PTIME (see Corollaries 4.2.8 and 4.3.7).

The thesis also contains examples of application of the techniques to modal deductive databases. Our methods for both of the problems of estimating space requirement for propositional modal logics and of constructing the least models for positive modal logic programs are applicable not only for the logics considered in the thesis.