owl - 一阶逻辑支持哪些描述逻辑不支持？

Question

在学习描述逻辑 (DL) 时，通常会读到它是一阶逻辑 (FOL) 的一个片段，但是很难明确地阅读一些从属于 FOL 的 DL 中排除的内容，这使得 DL (及其所有方言 ALC、SHOIN 等...)可确定。
或者换句话说，你能不能给我提供一些 FOL 中无法表达的例子
通过 DL(以及哪些是 FOL 中半/不可判定性的原因)？

Answer 1

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

(一种形式)树模型属性——这个属性对于表格方法很重要；

可嵌入到多模态系统中——众所周知，这些系统是“稳健可判定的”；

可嵌入到所谓的 FOL protected 片段中——见下文；

可嵌入到两个变量的 FOL 片段中——这是可判定的；

地区——见下文。

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

所在地 (摘自《描述逻辑手册》，第二版，第 3.6 节):

One of the main reasons why satisfiability and subsumption in many Description Logics are decidable – although highly complex – is that most of the concept constructors can express only local properties about an element 〈...〉 Intuitively, this implies that a constraint regarding x will not “talk about” elements which are arbitrarily far (w.r.t. role links) from x. This also means that in ALC, and in many Description Logics, an assertion on an individual cannot state properties about a whole structure satisfying it. However, not every Description Logic satisfies locality.

protected 碎片 (摘自 The Description Logic Handbook，第 2 版，第 4.2.3 节)

Guarded fragments are obtained from first-order logic by allowing the use of quantified variables only if these variables are guarded by appropriate atoms before they are used in the body of a formula. More precisely, quantifiers are restricted to appear only in the form
     ∃y(P(x,y) ∧ Φ(y))         or      ∀y(P(x,y) ⊃ Φ(y))               (First Guarded Fragment)
     ∃y(P(x,y) ∧ Φ(x,y))      or      ∀y(P(x,y) ⊃ Φ(x,y))            (Guarded Fragment)
for atoms P, vectors of variables x and y and (first) guarded fragment formulae Φ with free variables in y and x (resp. in y).

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

∀x.(C(X) ↔ ∃y.(likes(x,y) ∧ ∃z.(likes(y,z) ∧ likes(z,x))))

∀x.(C(x) ↔ ∃z.(favoriteTeacher(x,z) ∧ firstGradeTeacherOf(x,z)))

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