The complexity of decision problems for modal propositional ogics

• Main Authors: Chen, Cheng-Chia, 陳正佳
• Other Authors: Lin, I-Peng
• Format: Others
• Language: zh-TW
• Published: 1993
• Online Access: http://ndltd.ncl.edu.tw/handle/90339243948035929602

博士 === 國立臺灣大學 === 資訊工程研究所 === 81 === In this dissertation we will investigate the computational complexity of decision problems for various modal propositional logics and their Horn fragments. In the first part we will show that every logic between C and S4/S8 is PSPACE-hard and,in particular, for C, CT, CS4, S2, S3, S6, S7 and S8, each is PSPACE-complete. Similarly, every logic between C and B will be shown to be PSPACE-hard and each logic between C and B such as OB, OB+, OM, OM+, KB and B will be shown to be PSPACE-complete. Finally, each of the following logics: K4In, S4In, K4Bn, S4Bn, S3.5, S9 and all extensions of K5 will be shown to have an NP- complete satisfiability problem. We then in the second part continue to study the complexity of the satisfiability problem for the Horn fragments of various modal logics. Our results show that we cannot benefit in efficiency of computation of the satisfiability problem for any logic between C and S4/S8/B by restricting the input to modal Horn formulas. Similar result also holds for the logic S4.3, but for extensions of K5 such as K5, KD5, K45, KD45 and S5, the satisfiability problem for their Horn fragments will be shown to be solvable in polynominal time. In the third part we present complexity results of other kinds of decision problems called the global deducibility relations and the global consistency relations, respectively. We can show that, for every logic between K and B, the global consistency relation as well as the global deducibility relation is EXPTIME-hard; in particuar, for K, T and B, their global deducibility relations and global consistency relations are all EXPTIME-complete. Finally, we study the complexity of the quantitative modal logic proposed by Lau and Lin and find that,like their qualitative versions, the satisfiability probelms for the quantitative K, D and T are all PSPACE- complete.