
194 Foundations of Semantic Web Technologies
will not be successful, which shows that tweety could be in the class Human
according to the knowledge base.
We obtain NNF(K
0
) = {¬H t ∃P.H, B(t), H(t)}. The tableau is initial-
ized with one node t and L(t) = {B, H}. Applying the TBox rule yields
L(t) ← ¬H t ∃P.H. Expanding this TBox axiom using the t-rule results
in L(t) ← ∃P.H since the addition of ¬H to L(t) would immediately yield
a contradiction. We now apply the ∃-rule and create a node with label x,
L(t, x) = {P }, and L(x) = {H}. At this stage, the node x is blocked by t,
and no further expansion of the tableau is possible.
t
P
L(t) = {H, B, ¬H t