Combining Terminological Logics with Tense Logic
Combining Terminological Logics with Tense Logic
复制标题
将术语逻辑与时态逻辑相结合
DOI：
10.1007/3-540-57287-2_41
复制
发表时间：
1993
期刊：
影响因子：
--
通讯作者：
K. Schild
中科院分区：
文献类型：
--
作者：
K. Schild
我们展示了如何向术语逻辑添加完整的一阶时间表达能力。这可以通过在命题封闭概念语言(如ALC)中嵌入基于点的时态运算符来实现。由此产生的时间术语逻辑在线性的、Dedekind完整时间上是完全可表达的，例如ℕ和ℝ，因为在这些时间结构上的所有一阶时间公式都是可表达的。然后，我们证明了用线性、离散、无界时间上的面向未来的时态算子来扩充ALC并不会增加其计算复杂性。为了建立这一复杂性结果，我们证明了由功能角色及其传递闭包增强的ALC中的一致性在多项式空间中是可计算的。最后，我们展示了如何直接获得术语逻辑的公理化和基于Tableau的张量逻辑扩展算法。
We show how to add full first-order temporal expressiveness to terminological logics. This can be achieved by embedding point-based tense operators in propositionally closed concept languages like ALC. The resulting temporal terminological logics are fully expressive over linear, Dedekind complete time such as ℕ and ℝ in the sense that all first-order temporal formulae over these time structures are expressible. We then prove that augmenting ALC by future-oriented tense operators interpreted over linear, discrete, unbounded time like IN does not increase its computational complexity. To establish this complexity result we show that coherence in ALC augmented by functional roles and their transitive closure is computable in polynomial space. We finally show how to obtain directly an axiomatization and a tableau-based algorithm for the tenselogical extension of terminological logics.