Я пытаюсь решить следующий пример, используя алгоритм таблиц для ALC. Учитывая следующее TBox T:
A⊆B
A⊆C
B⊆∃R.D̸
C⊆∃R.D
E⊆∀R.D̸
Скажите, является ли понятие А выполнимым. Поэтому я поставил A (a) в свой ABox и запустил алгоритм, получив:
A0={((A̸∨B)∩(A̸∨C)∩(B̸∨∃R.D̸)∩(C̸∨∃R.D)∩(E̸∨∀R.D̸))(a)}.
Тогда я получаю:
A1={((A̸∨B),(A̸∨C),(B̸∨∃R.D̸),(C̸∨∃R.D),(E̸∨∀R.D̸))(a)}.
, что приводит меня к:
Ak={((A̸(a)∨B(a)),(A̸(a)∨C(a)),(B̸(a)∨R(a,b)D(b̸)),(C̸(a)∨R(a,c)D(c)),(E̸(a)∨D̸(b)))}.
A̸ (a) - это столкновение с A (a), B̸ (a) - это столкновение с B (a), а C̸ (a) - это столкновение с C (a), поэтому у меня есть:
Ak={((B(a)),(C(a)),(R(a,b)D(b̸)),(R(b,c)D(c)),(E̸(a)∨D̸(b)))}.
Давайте посмотрим, что происходит с расширением b:
Ak+1={((A̸∨B),(A̸∨C),(B̸∨∃R.D̸),(C̸∨∃R.D),(E̸∨∀R.D̸))(b)}.
что приводит меня к:
Ak+m={((A̸(b)∨B(b)),(A̸(b)∨C(b)),(B̸(b)∨blocked),(C̸(b)∨blocked),(E̸(b)∨D̸(c)))}.
Теперь D̸ (c) конфликтует с D (c) и B̸ (b) конфликтует с B (b).
И я понимаю, что это неудовлетворительно, что неправильно. Может кто-нибудь показать мне, где я не прав с применением этого алгоритма таблицы?