Foundations of Semantic Web Technologies

204 Foundations of Semantic Web Technologies

We now apply the ∀-rule to ∀P.h ∈ L(x): j is a C-predecessor of x, and

hence a P

−

-predecessor of x due to C v P

−

. So j is a P

−

-neighbor of x, and

the ∀-rule yields L(j) ← h. Since we already have ¬h ∈ L(j), the algorithm

terminates with the tableau containing a contradiction.

L(j) = {∃C.h, ¬h, h}

j

C

//

x

L(x) = {h, ¬h t ∀P.h, ∀P.h}

5.3.4.3.4 Transitivity and Blocking The next example displays block-

ing and the effect of the trans-rule. Consider the knowledge bas e K = {h v

∃F.>, F v A, ∀A.h(j), h(j), ≥F.>(j), A ◦ A v A}, which stands for the fol-

lowing.

Human v ∃hasFather.>

hasFather v hasAncestor

∀hasAncestor