Пример алгоритма таблицы ALC
Я пытаюсь решить следующий пример, используя алгоритм таблицы для 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).
И я получаю это неудовлетворительно, что неправильно. Может ли кто-нибудь показать мне, где я не прав с применением этого алгоритма таблицы?