First-Order Rewritability and Complexity of Two-Dimensional Temporal Ontology-Mediated Queries
First-Order Rewritability and Complexity of Two-Dimensional Temporal Ontology-Mediated Queries
复制标题
DOI：
10.1613/jair.1.13511
复制
发表时间：
2021-11
期刊：
影响因子：
--
通讯作者：
A. Artale;R. Kontchakov;Alisa Kovtunova;V. Ryzhikov;F. Wolter;M. Zakharyaschev
中科院分区：
文献类型：
--
作者：
A. Artale;R. Kontchakov;Alisa Kovtunova;V. Ryzhikov;F. Wolter;M. Zakharyaschev
针对基于本体的时态数据访问问题，将扩展的DL-Lite族逻辑与允许关系原语递归的离散时间（Z，1，FO）线性时态逻辑LTL（RPR）相结合，设计了二维时态本体和查询语言.在电路复杂性方面，FO（<，RPR）-和FO（RPR）-可重写性分别保证在统一AC 0和NC 1中回答OMQ。我们分三步进行。首先，我们定义了一个层次结构的二维DL-Lite/LTL本体语言和原子查询的OMQ的FO重写性，通过构建到一维LTL OMQ的投影，并采用最近的结果的FO重写命题LTL OMQ。由于预测涉及确定本体和数据的一致性，我们也考虑了我们的语言的一致性问题。虽然不确定性的一致性与表达布尔角色夹杂物的2D本体语言可能是预期的，我们还表明，而令人惊讶的是，限制克罗姆和霍恩的角色夹杂物导致可判定性（和ExpSpace完整性），即使一个承认完整的布尔概念。作为最后一步，我们解除原子OMQ的可重写性结果的OMQ与表达积极的时态实例查询。提升结果是基于对规范模型的深入研究，并且只涉及Horn本体。
Aiming at ontology-based data access to temporal data, we design two-dimensional temporal ontology and query languages by combining logics from the (extended) DL-Lite family with linear temporal logic LTL over discrete time (Z, 1, and FO(RPR) that admits relational primitive recursion. In terms of circuit complexity, FO(<, ≡)- and FO(RPR)-rewritability guarantee answering OMQs in uniform AC0 and NC1, respectively. We proceed in three steps. First, we define a hierarchy of 2D DL-Lite/LTL ontology languages and investigate the FO-rewritability of OMQs with atomic queries by constructing projections onto 1D LTL OMQs and employing recent results on the FO-rewritability of propositional LTL OMQs. As the projections involve deciding consistency of ontologies and data, we also consider the consistency problem for our languages. While the undecidability of consistency for 2D ontology languages with expressive Boolean role inclusions might be expected, we also show that, rather surprisingly, the restriction to Krom and Horn role inclusions leads to decidability (and ExpSpace-completeness), even if one admits full Booleans on concepts. As a final step, we lift some of the rewritability results for atomic OMQs to OMQs with expressive positive temporal instance queries. The lifting results are based on an in-depth study of the canonical models and only concern Horn ontologies.