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

Question

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

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

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

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

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

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

Answer 1

Доказать, что что-то не может быть выражено в логике описания, сложно. Есть несколько способов сделать это. Например, рассмотрите фрагмент FOL, который может выражать весь SROIQ, добавьте к нему фрагмент FOL, который охватывает ваш случай, и изучите сложность получающейся логики. Если сложность строго выше, чем у SROIQ, то явно SROIQ недостаточно, чтобы выразить то, что вы хотите. Вы также можете изучить формы моделей. Например, в ALC всегда есть конечные модели любого согласованного KB. Если, добавляя новые конструкции, вы можете показать, что должно быть бесконечное количество моделей, вы не можете выразить свои конструкции в 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
    ] .