QCRs против функционального свойства

Question

У меня есть вопрос по теме:

SOF - головоломка Эйнштейна в OWL

В сове все ограничения мощности основаны на функциональных и обратных функциональных свойствах свойств объекта. Я переделал его с помощью QCR.

Старая модель (пример):

man drinks some beverage;
drinks -> functional, inferse functional

Новая модель / EDITED /:

man drinks exactly 1 beverage;
beverage drinkedBy exactly 1 man;
drinks -> domain:man, range:beverage
drinkedBy -> domain:beverage, range:man
drinks inverseOf drinkedBy

Я заменил все "некоторые" на "ровно 1". Я думаю, что первый тип эквивалентен второй модели, но рассудок FaCT++ зависает после 15 секунд его запуска (3+ ГБ ОЗУ потрачено впустую и заморожено). HermiT не замерзает, но он не может вывести ничего, кроме подклассов.

Финальный файл / РЕДАКТОР /: FS или MR

Спасибо за ответ.

Answer 1

После дополнительного обсуждения с Денисом он объяснил мне проблему.

В основном модель верна, но необходимо реализовать, чтобы в каждом доме было максимум по одному соседу слева / справа. Рассмотрим ситуацию: H5 слева H4 слева H3 слева H2 слева H1 и дополнительный H5 слева H3 В исходной модели это невозможно, поскольку (обратный) функционал не позволяет этого. (Если H5 покинул H4, то H5 не может покинуть H3). В нашей модели у нас больше нет ограничений на left_to / right_to. Таким образом, рассматриваемая ситуация является действительной.

Чтобы решить эту проблему, нам нужно добавить еще одно утверждение: House SubClassOf left_to max 1 House / или / House SubClassOf right_to max 1 House

Таким образом, результат: QCR с max 1 = функционал, но модель была неправильной.

Answer 2

Эти три аксиомы

1. Человек SubClassOf пьет немного напитков
   
   • Человек ∃ ∃ пьет. Напиток
2. напитки: функциональные, обратные функциональные
   
   • Вещи ⊑ ≤1 напитки.
   • Вещи ⊑ ≤1 напитки^-1.

логически не эквивалентны

3. Man SubClassOf пьет ровно 1 напиток
   • Мужчина ⊑ =1 напиток. Напиток

Вот некоторые данные, которые несовместимы в первой модели, но не во второй:

m1 rdf: тип Man.
d1 rdf: тип Напиток.
d2 rdf: тип (не напиток).
m1 напитки d1, d2.

"Свойство p является функциональным" эквивалентно аксиоме "Thing p max 1 Thing".

Answer 3

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

Редактировать: обсудили это с Дмитрием Царковым (главный разработчик FaCT++). Он отметил, что функциональная характеристика эквивалентна максимум 1 количеству элементов. ровно 1 кардинальность включает в себя существование, что означает, что у рассудителя есть разные таблицы для исследования, которые были бы более сложными. Я указал ему на этот вопрос, чтобы дать более полный ответ.