二维时序本体中介查询的首阶可重写性与复杂性

面向时序数据的基于本体的数据访问，我们通过将（扩展）DL-Lite 族中的逻辑与离散时间（Z,<）上的线性时序逻辑 LTL 相结合，设计了二维时序本体与查询语言。我们主要关注由 2D 本体和正时序实例查询组成的本体中介查询（OMQ）的首阶可重写性。我们 FO 重写的目标语言是二排序 FO(<)——带时间瞬间排序（由内建前序关系 < 给出）与个体域排序的一阶逻辑——其扩展 FOE（带标准同余谓词 t ≡ 0 mod n，对任意固定 n > 1）以及允许关系原语递归的 FO(RPR)。就电路复杂性而言，FOE- 与 FO(RPR)-可重写性分别保证 OMQ 在一致 AC0 与 NC1 中应答。我们分三步推进。首先，我们定义 2D DL-Lite/LTL 本体语言层次，并通过构造到 1D LTL OMQ 的投影并利用近期关于命题 LTL OMQ 首阶可重写性的结果，研究带原子查询的 OMQ 的 FO 可重写性。由于投影涉及判定本体与数据的一致性，我们也考虑所设语言的一致性问题。虽然带表达性布尔角色包含的 2D 本体语言一致性的不可判定性或可预期，我们也展示出，颇令人惊讶地，限制为 Krom 与 Horn 角色包含（即便允许概念上完全布尔）可获可判定性（且为 ExpSpace-完全）。作为最后一步，我们将部分原子 OMQ 的重写结果提升到带表达性正时序实例查询的 OMQ。提升结果基于对典范模型的深入研究，且仅涉及 Horn 本体。