A note on the complexity of the satisfiability of modal Horn clauses

AbstractA bottom-up algorithm is given for testing the satisfiability of sets of propositional modal Horn clauses. For some modal logics, such as S5, the algorithm works in polynomial time, while for other modal logics, like K, Q, T, and S4, the worst case complexity can be considerably higher