Почему OWL Full неразрешима?

Question

Я все время думал о том, почему OWL Full неразрешима, но я не нашел простого для понимания примера, который заставил бы меня понять его.

Я нашел утверждения, которые объясняют, что это происходит из-за "Завершения Entailment", и это также связано с тем фактом, что 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 и, возможно, нескольким другим до и после того же курса может помочь.

Кстати, неразрешимость и невозможность закрытия вычислительного вложения - это не одно и то же.

Answer 3

Хотя набор математических конструкторов OWL Full и OWL DL идентичен, OWL Full не имеет ограничений на использование этих конструкторов; Подумайте об отсутствии ограничений на использование переходных свойств, чтобы понять, почему OWL Full неразрешима.

Answer 4

Для меня самый простой способ понять неразрешимость OWL Full - это посмотреть на глобальные ограничения OWL 2 DL, в частности, на роль простых ролей: https://www.w3.org/TR/owl2-syntax/. Только OWL 2 DL с этими снятыми ограничениями неразрешима, так же как и OWL 2 Full, в котором они есть.

Эти слайды http://www.cs.man.ac.uk/~horrocks/Slides/ijcai-slides.pdf содержат ссылки, почему ослабление (некоторые из) вышеуказанных ограничений делает логику неразрешимой.