Foundations of Fuzzy Logic and Semantic Web Languages

Fuzzy OWL 213

TABLE 10.10: The OR-based tableau rules for fuzzy ALC with empty TBox.

(var). For variable x

v:C

occurring in C

F

add x

v:C

∈ [0, 1] to C

F

. For variable

x

(v,w):R

occurring in C

F

add x

(v,w):R

∈ [0, 1] to C

F

.

(⊥). If ⊥ ∈ L(v) then C

F

:= C

F

∪ {x

v:⊥

= 0}.

(>). If > ∈ L(v) then C

F

:= C

F

∪ {x

v:>

= 1}.

(

¯

A). If ¬A ∈ L(v) then add A to L(v), and C

F

:= C

F

∪ {x

v:A

≤ 1 − x

v:¬A

}.

(u). If (i) C

1

uC

2

∈ L(v) and (ii) the rule has not been already applied to this

concept, then add C

1

and C

2

to L(v), and C

F

:= C

F

∪{x

v:C

1

⊗x

v:C

2

≥

x

v:C

1

uC

2

}.

(t). If (i) C

1

tC

2

∈ L(v) and (ii) the rule has not been already applied to this

concept, then add C

1

and C

2

to L(v), and C

F

:= C

F

∪{x

v:C

1

⊕x

v:C

2

≥

x

v:C

1

tC

2

}.

(∀). If (i) ∀R.C ∈ L(v), R ∈ L(hv, wi) and (ii) the rule has not been already

applied to this ...