EL-Concepts go Second-Order: Greatest Fixpoints and Simulation Quantifiers
EL-Concepts go Second-Order: Greatest Fixpoints and Simulation Quantifiers
复制标题
EL 概念进入二阶：最大固定点和模拟量词
DOI：
--
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
F. Wolter
中科院分区：
文献类型：
--
作者：
C. Lutz;R. Piro;F. Wolter
众所周知的描述逻辑（DL）ALC通常被认为是包含所有布尔概念构造器的基本DL，并且通过接纳附加概念构造器从其导出所有表达DL。 ALC 的基本作用很大程度上是由于它在逻辑、模型理论和计算特性方面表现良好。反过来，这种良好的行为可以通过以下事实得到很好的解释：ALC 概念可以精确地表征为一阶逻辑 (FO) 的互模拟不变片段，即当且仅当 FO 公式等价于 ALC 概念时，FO 公式在互模拟下是不变的 [22,13,16]。特别是，互模拟下的不变性解释了 ALC 的树模型特性及其有利的计算特性 [24]。在上述表征中，ALC 是 FO 片段的条件远不如其互模拟不变性重要。事实上，ALCμ是ALC与定点算子的扩展，它不是FO的片段，而是继承了ALC的几乎所有重要属性[8, 12]。与 ALC 类似，ALCμ 的基本作用（特别是模态 mu 演算的形式）可以通过以下事实来解释：ALCμ 概念可以精确地表征为一元二阶逻辑 (MSO) 的互模拟不变片段 [14, 8]。事实上，从纯粹的理论角度来看，很难解释为什么 ALC 而不是 ALCμ 构成了当前本体语言标准的逻辑基础； mu 微积分概念可能难以掌握，而且尽管理论复杂性相同，但 ALCμ 中的有效推理比 ALC 更具挑战性，这可能是 ALCμ 与 ALC 相比兴趣有限的唯一原因。近年来，超大型本体的开发以及使用本体来访问实例数据重新引起了人们对易于处理的深度学习的兴趣。主要示例是 EL [5] 和 DL-Lite [9]，它们分别是 OWL 配置文件 OWL2 EL 和 OWL2 QL 的逻辑基础。与 ALC 相比，此类 DL 的表达能力仍缺乏令人满意的表征，本文的首要目标是填补 EL 的这一空白。为此，我们将 EL 描述为 FO 的最大片段，它在模拟中保留并具有有限的最小模型。请注意，仅在模拟下保存就会使 EL 具有析取特征，并且最小模型的存在反映了 EL 的“喇叭方面”。然而，本文的第二个也是主要目的是介绍和研究 EL 的两个具有最大固定点的等表达扩展，即 EL 和 EL，以及 Proc。 23 日国际。描述逻辑研讨会 (DL2010)，CEUR-WS 573，加拿大滑铁卢，2010 年。
The well-known description logic (DL) ALC is usually regarded as the basic DL that comprises all Boolean concept constructors and from which all expressive DLs are derived by admitting additional concept constructors. The fundamental role of ALC is largely due to the fact that it is very well-behaved regarding its logical, model-theoretic, and computational properties. This good behavior can, in turn, be explained nicely by the fact that ALC-concepts can be characterized exactly as the bisimulation invariant fragment of first-order logic (FO) in the sense that an FO formula is invariant under bisimulation if, and only if, it is equivalent to an ALC-concept [22, 13, 16]. In particular, invariance under bisimulation explains the tree-model property of ALC as well as its favorable computational properties [24]. In the mentioned characterization, the condition thatALC is a fragment of FO is much less important than its bisimulation invariance. In fact, ALCμ, the extension of ALC with fixpoint operators, is not a fragment of FO, but inherits almost all important properties of ALC [8, 12]. Similar to ALC, ALCμ’s fundamental role (in particular in its formulation as the modal mu-calculus) can be explained by the fact that ALCμ-concepts can be characterized exactly as the bisimulation invariant fragment of monadic second-order logic (MSO) [14, 8]. Indeed, from a purely theoretical viewpoint it is hard to explain why ALC rather than ALCμ forms the logical underpinning of current ontology language standards; the facts that mu-calculus concepts can be hard to grasp and that, despite the same theoretical complexity, efficient reasoning in ALCμ is more challenging than in ALC are probably the only reasons for the limited interest in ALCμ compared to ALC. In recent years, the development of very large ontologies and the use of ontologies to access instance data has led to a revival of interest in tractable DLs. The main examples are EL [5] and DL-Lite [9], the logical underpinnings of the OWL profiles OWL2 EL and OWL2 QL, respectively. In contrast to ALC, a satisfactory characterization of the expressivity of such DLs is still missing, and a first aim of this paper is to fill this gap for EL. To this end, we characterize EL as a maximal fragment of FO that is preserved under simulations and has finite minimal models. Note that preservation under simulations alone would characterize EL with disjunctions, and the existence of minimal models reflects the “Horn-aspect” of EL. The second and main aim of this paper, however, is to introduce and investigate two equi-expressive extensions of EL with greatest fixpoints, EL and EL, and to Proc. 23rd Int. Workshop on Description Logics (DL2010), CEUR-WS 573, Waterloo, Canada, 2010.
DOI：
--
发表时间：
2010
期刊：
--
影响因子：
--
作者：
Boris Konev
通讯作者：
Boris Konev