owl - 为什么 OWL Full 不可判定？

Question

我一直在四处寻找为什么 OWL Full 是不可判定的，但我还没有找到一个易于理解的例子来让我理解它。

我发现一些陈述解释了这是由于“Entailment Closure”，并且这也与 OWL Full 可以同时拥有既是属性又是个体的类的事实相关。

但我不明白这些陈述之间的关系。

Answer 1

这里有一个例子应该足以理解为什么 OWL 2 Full 是不可判定的。这与Russel's paradox有关.

在 OWL Full 中，您可以定义一个将自身作为实例的类:

:IsInstanceOfItself  a  :IsIntanceOfItself .

这在 RDF/RDFS 中也是可能的，但它不会使逻辑不可判定。导致不可判定性的原因是您可以定义在 OWL 2 Full 中自相矛盾的类。您可以定义将自身作为实例的类的类:

:HaveThemselvesAsInstance
    rdfs:subClassOf  [
        a  owl:Restriction;
        owl:onProperty  rdf:type;
        owl:hasSelf  true
    ] .

然后你可以定义没有自己作为实例的类:

:DoNotHaveThemselvesAsInstance
    owl:equivalentClass  [ owl:complementOf  :HaveThemselvesAsInstance ] .

现在，我们可以问一个问题:是 :DoNotHaveThemselvesAsInstance自己的一个实例？假设是这样。然后:

:DoNotHaveThemselvesAsInstance  a  :DoNotHaveThemselvesAsInstance .

是真的。因此， :DoNotHaveThemselvesAsInstance遵守定义，它在一个与自身没有关系的类中，与 rdf:type属性(property)。所以假设是错误的。因此 :DoNotHaveThemselvesAsInstance必须是那些具有 rdf:type 的类的补充与他们自己。所以它必须是 :DoNotHaveThemselvesAsInstance 的一个实例.所以上面假设的关系应该成立。回到最初的步骤。因此，对于定义上面定义的类的任何本体，都不存在任何模型。所以不可能有一类没有自己作为实例的类。所以也许，所有的类都有自己作为实例，也许？但是存在一些本体模型，其中某些类不是它们自己的实例。所以... OWL 2 Full 真的完蛋了，不是吗？