Model Comparison Games for Horn Description Logics

Horn description logics are syntactically defined fragments of standard description logics that fall within the Horn fragment of first-order logic and for which ontology-mediated query answering is in PTIME for data complexity. They were independently introduced in modal logic to capture the intersection of Horn first-order logic with modal logic. In this paper, we introduce model comparison games for the basic Horn description logic $\pmb{horn}\mathcal{ALC}$ (corresponding to the basic Horn modal logic) and use them to obtain an Ehrenfeucht-Frafsse type definability result and a van Benthem style expressive completeness result for $\pmb{horn}\mathcal{ALC}$. We also establish a finite model theory version of the latter. The Ehrenfeucht-Frafsse type definability result is used to show that checking $\pmb{horn}\mathcal{ALC}$ indistinguishability of models is ExpTIME-complete, which is in sharp contrast to $\mathcal{ALC}$ indistinguishability (i.e., bisimulation equivalence) checkable in PTIME. In addition, we explore the behavior of Horn fragments of more expressive description and modal logics by defining a Horn guarded fragment of first-order logic and introducing model comparison games for it.