Foundations of Semantic Web Technologies

OWL Formal Semantics 189

b

S



L(b) = ∅

a

R

OO

R



L(a) = {A, ∃R.B}

c

L(c) = {A t B}

FIGURE 5.11: Example of an initial tableau given the knowledge base

K = {A(a), (∃R.B)(a), R(a, b), R(a, c), S(b, b), (A t B)(c), ¬A t (∀S.B)}

• directed edges between some pairs of nodes,

• for each node labeled x, a set L(x) of class expressions, and

• for each pair of nodes x and y, a set L(x, y) of role names.

When we depict a tableau, we omit edges which are labeled with the empty

set. Also, we make the agreement that > is contained in L(x), for any x, but

we often do not write it down, and in fact the algorithm does not explicitly

derive this.

Given an ALC knowledge base