| Summary: | 博士 === 國立臺灣大學 === 資訊工程研究所 === 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.
|
|---|
