The computational complexity of the satisfiability of modal Horn clauses for modal propositional logics (Q1329742): Difference between revisions

The complexity of modal Horn clause satisfiability is investigated, for several propositional logics. It is shown, in summary, that restricting the input formula to modal Horn clauses does not decrease the inherent complexity of the satisfiability problem. In particular, the satisfiability problem for any modal logic between K and S4 or between K and B is PSPACE-hard. Therefore, the satisfiability problem for modal Horn clauses is PSPACE- complete. Further variations and extentions of Kripke models are studied with respect to the satisfiability problem.