Abstract

Partly motivated by description logics, poor man's logics have been proposed as an interesting fragment of modal logics. A poor man's logic is a propositional modal logic where only literals and the connectives ∧, □, and ◊ are allowed. It is known that the complexity of the satisfiability problem may drop dramatically when going from a full modal logic to the corresponding poor man's logic, e.g., in the case of modal logic K one goes from PSPACE-complete to coNP-complete. We prove that it is sometimes possible to extend poor man's logics with restricted disjunctions (i.e., clauses) without increasing the computational complexity. For Horn and Krom clauses, we provide necessary and sufficient conditions for when the resulting logic is polynomial-time. Such extensions correspond to allowing a restricted use of the union operator in description logics.