In prior research with modal logic S5, restriction from general to Horn clause form yielded polynomial-time complexity for satisfiability, giving rise to hope that a similar situation might prevail for other modal logics. This paper’s results dash that hope in most prospective cases. The complexity of the satisfiability problem is PSPACE-hard for any logic between K and S4 or between K and B, which includes T; polynomial for S4.3 and extensions of K5 including K5, KD5, K45, KD45, and S5; and NP-complete for S4.3 and some linear tense logics closely related to S4.3, namely CL, SL, and PL.

The paper is self-contained and well organized, the abstract, introduction, and conclusion all relaying, in nuanced forms, the main results. I detected a tutorial flavor in the paper, at least regarding some methods and the logics. Though not intentionally a tutorial, the paper displays textbook clarity, for example, in the employment of problem reduction and KD5-satisfiability testing of K5 Horn clauses, presenting an algorithm with an accompanying step-by-step correctness proof. The definition of modal Horn clauses, which is not unified in the literature, is given in a referenced variant in both disjunctive and rule forms, with succinct  examples.  Complexity definitions and categories are assumed to be known, however. The tutorial aspect does not mean that new (derivative) ground has not been plowed. Neither does it mean that applications are developed, though programming languages are mentioned. The paper’s seeming door-closings on a range of topics coexist with door-openings for alternative or shorter proofs in some cases.