Как доказать, что что-то *не* может быть переведено в логику описания?

Моя интуиция подсказывает, что невозможно перевести предложение

все красные машины лучше всех синих

в логику описания (в FOL это было бы

∀x∀y (красный(x) ∧ синий(y) → лучше(x,y))

интерпретируется в области автомобилей). Действительно, единственной конструкцией, представляющей собой полное бинарное отношение, содержащее все пары элементов предметной области, является универсальная роль U. Я не вижу, как запросить все пары элементов множества красного слева и элементы множества синего справа, т. е. как ограничить U определенным набором предшественников и преемники.

Но незнание того, как это сделать, не является доказательством того, что это невозможно. Поэтому мой вопрос: когда вы работаете с определенной логикой описания (например, SROIQ, как описано здесь), как вы докажете, что в нем невозможно представить данное предложение естественного языка или формулу ЛЖ?


owl description-logic first-order-logic
person yannis    schedule 29.04.2017    source источник
comment
Ваш вопрос больше подходит для Math StackExchange или даже MathOverflow. Однако я думаю, что вам необходимо доказать, что ваша формула (или любая эквивалентная формула) не принадлежит так называемому защищенному фрагменту ВОЛ (точнее, ограниченному фрагменту ВОЛ, соответствующему SROIQ).   -  person Stanislav Kralin    schedule 05.05.2017

Ответы (1)


arrow_upward
2
arrow_downward

Доказать, что что-то не может быть выражено в логике описания, сложно. Есть несколько способов сделать это. Например, рассмотрите фрагмент FOL, который может выражать весь SROIQ, добавьте к нему фрагмент FOL, который охватывает ваш случай, и изучите сложность полученной логики. Если сложность строго выше, чем у SROIQ, то очевидно, что SROIQ недостаточно для выражения того, что вы хотите. Вы также можете изучить формы моделей. Например, в ALC всегда есть конечные модели любой непротиворечивой базы знаний. Если, добавляя новые конструкции, вы можете показать, что должны быть бесконечные модели, то вы не сможете выразить свои конструкции в ALC. И т.п.

Вернемся к вашему конкретному случаю, когда все красные машины лучше, чем все синие (утверждение, которое весьма спорно!). Вы не доказываете, что это нельзя выразить в SROIQ, потому что это возможно! Этот вид конструкций (называемый концепт-продукт, поскольку он соответствует декартовому произведению двух классов, а именно red и blue в вашем случае) рассматривается в исследовательской статье 2008 года под названием Все слоны больше всех мышей Рудольфа, Крётча и Хитцлера. В статье доказывается, что концептуальные продукты могут быть выражены в OWL 2 DL, и объясняется, как это можно сделать в целом.

Это делается следующим образом в OWL, сериализованном в синтаксисе Turtle (:r1 и :r2 должны быть свежими именами ролей, нигде больше не используемыми, а :x должно быть новым индивидуальным именем, нигде больше не используемым):

:r1 a owl:ObjectProperty .
:r2 a owl:ObjectProperty .
:x a owl:Thing .
:better a owl:ObjectProperty;
    owl:propertyChainAxiom (:r1 :r2) .
:Red a owl:Class;
    rdfs:subClassOf [
        a owl:Restriction;
        owl:onProperty :r1;
        owl:hasValue :x
    ] .
 :Blue a owl:Class;
    rdfs:subClassOf [
        a owl:Restriction;
        owl:onProperty [owl:inverseOf :r2];
        owl:hasValue :x
    ] .
person Antoine Zimmermann    schedule 06.05.2017