为什么OWL Full无法确定？

Question

我一直在寻找为什么OWL Full无法确定的原因，但是我还没有找到一个易于理解的示例来使我理解它。

我发现有陈述解释这是由于“封闭性”引起的，并且还与OWL Full可以同时具有作为属性的类和也作为个人的类这一事实有关。

但是我不理解这些陈述之间的关系。

Answer 1

这里有一个例子应该足以理解为什么 OWL 2 Full 是不可判定的。这与罗素悖论有关。

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

Answer 2

你的问题很有意义，但很难回答。此外，OWL-DL 和 OWL-Full 之间的区别并不固定。最初在 OWL 中受到限制的某些内容后来被允许，最流行的情况是双关语。

但基本上，这个想法是能够编写一个推理器，可以回答是或否，并避免不知道或“无限”不知道。这个 30 分钟的Tableaux 算法讲座以及同一课程前后的其他几个讲座可能会有所帮助。

顺便说一下，计算蕴涵闭包的不可判定性和不可能性不是一回事。