一句话：为 Horn 描述逻辑 hornALC 引入模型比较博弈，给出可定义性与表达完全性结果，并证明其不可区分性检查为 ExpTime 完全。
Horn 描述逻辑是标准描述逻辑中对应一阶 Horn 片段的句法片段，其本体中介查询回答在数据复杂度下为 PTime。本文为基本 Horn 描述逻辑 hornALC（对应基本 Horn 模态逻辑）引入模型比较博弈，并据此建立 Ehrenfeucht–Fraïssé 型可定义性结果和 van Benthem 型表达完全性结果，同时给出后者的有限模型论版本。作者进一步利用该可定义性结果证明 hornALC 模型不可区分性检查是 ExpTime 完全的，这与 ALC 的不可区分性（即互模拟等价）可在 PTime 检查形成鲜明对比。最后，文章定义一阶 Horn 守卫片段并引入相应模型比较博弈，以探索更强描述逻辑与模态逻辑的 Horn 片段。
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 hornALC (corresponding to the basic Horn modal logic) and use them to obtain an Ehrenfeucht-Fraïssé type definability result and a van Benthem style expressive completeness result for hornALC. We also establish a finite model theory version of the latter. The Ehrenfeucht-Fraïssé type definability result is used to show that checking hornALC indistinguishability of models is ExpTime-complete, which is in sharp contrast to 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.