Combining CPDL (Propositional Dynamic Logic with Converse) and regular grammar logic results in an expressive modal logic denoted by CPDL
reg
. This logic covers TEAMLOG, a logical formalism used to express properties of agents’ cooperation in terms of beliefs, goals and intentions. It can also be used as a description logic for expressing terminological knowledge, in which both regular role inclusion axioms and CPDL-like role constructors are allowed. In this paper, we develop an expressive and tractable rule language called Horn-CPDL
reg
. As a special property, this rule language allows the concept constructor “universal restriction” to appear on the left hand side of general concept inclusion axioms. We use a special semantics for Horn-CPDL
reg
that is based on pseudo-interpretations. It is called the constructive semantics and coincides with the traditional semantics when the concept constructor “universal restriction” is disallowed on the left hand side of concept inclusion axioms or when the language is used as an epistemic formalism and the accessibility relations are serial. We provide an algorithm with PTIME data complexity for checking whether a knowledge base in Horn-CPDL
reg
has a pseudo-model. This shows that the instance checking problem in Horn-CPDL
reg
with respect to the constructive semantics has PTIME data complexity.
