First-Order Rewritability of Ontology-Mediated Queries in Linear Temporal Logic
First-Order Rewritability of Ontology-Mediated Queries in Linear Temporal Logic
复制标题
DOI：
10.1016/j.artint.2021.103536
复制
发表时间：
2020-04
期刊：
影响因子：
--
通讯作者：
A. Artale;R. Kontchakov;Alisa Kovtunova;V. Ryzhikov;F. Wolter;M. Zakharyaschev
中科院分区：
文献类型：
--
作者：
A. Artale;R. Kontchakov;Alisa Kovtunova;V. Ryzhikov;F. Wolter;M. Zakharyaschev
我们调查基于本体的数据访问时态数据。我们考虑在离散时间（Z，<）上解释的线性时态逻辑LTL中给出的时态本体。在LTL或MFO（<）中给出，一元一阶逻辑具有内置的线性顺序。我们关心的是一阶重写本体介导的查询（OMQs）组成的时间本体和查询。通过考虑本体中使用的时态运算符，并区分完整LTL及其核心Krom和Horn片段中给出的本体，我们通过证明可重写为FO（<），具有内置线性顺序的一阶逻辑，或FO（<，n），其扩展FO（<）具有标准算术谓词x 0（mod n），对于任何固定的n> 1，或FO（RPR），它用关系原语递归扩展FO（<）。在电路复杂性方面，FO（<，RPR）-和FO（RPR）-可重写性保证了OMQ分别在统一的图像1和图像2中回答。我们获得了类似的层次结构更有表现力的查询类型：积极的LTL-公式，单调MFO（<）-和任意MFO（<）-公式。我们的研究结果是直接适用的，如果要访问的时态数据是一维的，而且，他们奠定了基础，调查基于本体的访问使用组合的时间和描述逻辑在二维时态数据。
We investigate ontology-based data access to temporal data. We consider temporal ontologies given in linear temporal logic LTL interpreted over discrete time (Z,<). Queries are given in LTL or MFO (<), monadic first-order logic with a built-in linear order. Our concern is first-order rewritability of ontology-mediated queries (OMQs) consisting of a temporal ontology and a query. By taking account of the temporal operators used in the ontology and distinguishing between ontologies given in full LTL and its core, Krom and Horn fragments, we identify a hierarchy of OMQs with atomic queries by proving rewritability into either FO (<), first-order logic with the built-in linear order, or FO (<,≡), which extends FO (<) with the standard arithmetic predicates x≡ 0 (mod n), for any fixed n> 1, or FO (RPR), which extends FO (<) with relational primitive recursion. In terms of circuit complexity, FO (<,≡)-and FO (RPR)-rewritability guarantee OMQ answering in uniform Image 1 and, respectively, Image 2. We obtain similar hierarchies for more expressive types of queries: positive LTL-formulas, monotone MFO (<)-and arbitrary MFO (<)-formulas. Our results are directly applicable if the temporal data to be accessed is one-dimensional; moreover, they lay foundations for investigating ontology-based access using combinations of temporal and description logics over two-dimensional temporal data.