A Cookbook for Temporal Conceptual Data Modelling with Description Logics
A Cookbook for Temporal Conceptual Data Modelling with Description Logics
复制标题
DOI：
10.1145/2629565
复制
发表时间：
2012-09
期刊：
影响因子：
--
通讯作者：
A. Artale;R. Kontchakov;V. Ryzhikov;M. Zakharyaschev
中科院分区：
文献类型：
--
作者：
A. Artale;R. Kontchakov;V. Ryzhikov;M. Zakharyaschev
我们设计了适用于对时态概念数据模型进行推理的时态描述逻辑（TDL），并研究了它们的计算复杂性。我们的形式体系基于具有三种概念包含类型（从原子概念包含和不相交到完全布尔型）以及基数约束和角色包含的DL - Lite逻辑。这些逻辑是在对象域的笛卡尔积和时间流（整数集，小于关系）上进行解释的，满足常量域假设。TBox的概念和角色包含在所有时刻（全局地）都成立，ABox的数据断言在指定的时刻成立。为了表达概念数据模型的时态约束，这些语言配备了灵活和刚性角色、概念上的标准未来和过去时态算子，以及角色上的“总是”和“有时”算子。我们最具表达力的TDL（它可以捕捉生命周期基数以及定性或定量的演化约束）结果是不可判定的。然而，通过省略概念/角色上的一些时态算子，或者通过限制概念包含的形式，我们构建了复杂性在NLogSpace和PSpace之间的逻辑。这些积极的结果是通过归约到命题时态逻辑的各种子句片段而获得的，这为使用命题或一阶时态证明器对时态数据模型进行推理开辟了一条道路。
We design temporal description logics (TDLs) suitable for reasoning about temporal conceptual data models and investigate their computational complexity. Our formalisms are based on DL-Lite logics with three types of concept inclusions (ranging from atomic concept inclusions and disjointness to the full Booleans), as well as cardinality constraints and role inclusions. The logics are interpreted over the Cartesian products of object domains and the flow of time (ℤ, <), satisfying the constant domain assumption. Concept and role inclusions of the TBox hold at all moments of time (globally), and data assertions of the ABox hold at specified moments of time. To express temporal constraints of conceptual data models, the languages are equipped with flexible and rigid roles, standard future and past temporal operators on concepts, and operators “always” and “sometime” on roles. The most expressive of our TDLs (which can capture lifespan cardinalities and either qualitative or quantitative evolution constraints) turns out to be undecidable. However, by omitting some of the temporal operators on concepts/roles or by restricting the form of concept inclusions, we construct logics whose complexity ranges between NLogSpace and PSpace. These positive results are obtained by reduction to various clausal fragments of propositional temporal logic, which opens a way to employ propositional or first-order temporal provers for reasoning about temporal data models.