我正在尝试使用 ALC 的 tableau 算法来解决以下示例。给定以下 TBox T：
A⊆B
A⊆C
B⊆∃R.D̸
C⊆∃R.D
E⊆∀R.D̸
判断概念 A 是否可满足。所以我把 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) 发生冲突。
我知道它是不可满足的，这是错误的。有人可以告诉我这个画面算法的应用我哪里错了吗？