13

在研究描述逻辑 (DL) 时，很常见的是它是一阶逻辑 (FOL) 的一个片段，但是很难明确地阅读 DL 中排除的内容，这是 FOL 的一部分，这使得 DL （及其所有方言 ALC、SHOIN 等...）可判定。或者换句话说，您能否在 FOL 中提供一些无法通过 DL 表达的示例（这也是 FOL 中半/不可判定性的原因）？

4

2 回答 2

5

以下关于描述逻辑的事实与可判定性密切相关：

  1. （一种）树模型属性——这个属性对于表格方法很重要；
  2. 可嵌入到多模式系统中——众所周知，多模式系统是“可确定的”；
  3. 可嵌入到所谓的 FOL 保护片段中——见下文；
  4. 可嵌入到两变量 FOL 片段中——这是可判定的；
  5. 地点——见下文。

其中一些事实是句法的，而一些是语义的。下面是描述逻辑的两个有趣的、与可判定性相关的、或多或少的句法特征：

位置（来自描述逻辑手册，第 2 版，第 3.6 节）：

许多描述逻辑中的可满足性和包含性是可判定的（尽管非常复杂）的主要原因之一是大多数概念构造函数只能表达关于元素的局部属性 <...> 直观地说，这意味着关于x的约束将不要“谈论”与x任意距离（wrt 角色链接）的元素。这也意味着在 ALC和许多描述逻辑中，对个体的断言不能陈述关于满足它的整个结构的属性。然而，并不是每个描述逻辑都满足局部性。

受保护的片段（来自描述逻辑手册，第 2 版，第 4.2.3 节）

保护片段是通过允许使用量化变量从一阶逻辑获得的，前提是这些变量在用于公式主体之前由适当的原子保护。更准确地说，量词被限制为仅以
     ∃<strong>y( P ( x , y ) ∧ Φ( y )) 或 ∀ y ( P ( x , y ) ⊃ Φ( y )) 形式出现（第一保护片段)
     ∃<strong>y( P ( x , y ) ∧ Φ( x , y )) 或 ∀ y( P ( x , y ) ⊃ Φ( x , y ))
原子P的（受保护片段），变量x和y的向量以及（第一个）受保护片段公式 Φ 与y和x中的自由变量（分别在y中） .

从这些角度，分析@JoshuaTaylor 评论中的例子：

  • ∀x.(C(X) ↔ ∃y.(喜欢(x,y) ∧ ∃z.(喜欢(y,z) ∧ 喜欢(z,x))))
  • ∀x.(C(x) ↔ ∃z.(favoriteTeacher(x,z) ∧ firstGradeTeacherOf(x,z)))

DL 在知识表示方面优于 FOL 的原因不仅与可判定性或计算复杂性有关。请看名为“FOL 作为语义 Web 语言？”的幻灯片。在本次讲座中。

于 2017-11-06T22:25:03.820 回答
2

正如 Turing 和 Church 所示，FOL 是不可判定的，因为没有算法可以确定 FOL 公式是否有效。很多描述逻辑是一阶逻辑的可判定片段，但也有一些描述逻辑比 FOL 具有更多的特征，许多空间、时间和模糊描述逻辑也是不可判定的。

于 2017-10-30T10:26:32.173 回答