The complexity of propositional modal theories and the complexity of consistency of propositional modal theories

Abstract

This paper is concerned with the computational complexity of the following problems for various modal logics L: (1). The L-deducibility problem: given a finite set of formulas S and a formula A, determine if A is in the modal theory T HL(S) formed with all theorems of the modal logic L as logical axioms and with all members of S as proper axioms. (2). The L-consistency problem: given a finite set of formulas S, determine if the theory THL(S) is consistent. Table 1 is a comparison of complexity results of these two problems and the corresponding provability and satisfiability problems for modal logics K, T, B, S4, KD45 and S5. The complexity results of the deducibility problem for extensions of K4 are a direct consequence of a modal deduction theorem for K4 (cf. [17, 15]). The NP-completeness of the S4-consistency problem is due to Tiomkin and Kaminski [15]. The main contribution of this paper is that we can show that the deducibility problem and the consistency problem for any modal logic between K and B are EXPTIME-hard; in particular, for K, T and B, both problems are EXPTIME-complete.