Database Reference
In-Depth Information
Lemma 3 shows the soundness of our algorithm. We prove, in next subsection, the converse (the
completeness) also holds. We show that provided the completion forest has been sufficiently ex-
panded, a mapping from
q
to can be constructed from a single canonical model.
Fuzzy Tableaux and Canonical models
The construction of the canonical model I
F
for is divided into two steps. First, is unravelled
into a fuzzy tableau. Then, the canonical model is induced from the tableau. The interpretation domain
D
I
F
of I
F
consists of a set of (maybe infinite) paths. The reason lies in that a KB may have infinite
models, whereas the canonical model I
F
is constructed from , which is a finite representation de-
cided by the termination of the algorithm. This requires some nodes in represent several elements in
D
I
F
. The paths is chosen to distinguish different elements represented in by the same node. The
definition of fuzzy tableau is based on the one in (Stoilos et al., 2006, 2007).
Definition 10.
(Fuzzy tableau) Let
K
, , be a
if
-SHIF (
D
KB,
R
,
R
D
the sets of abstract
and concrete roles occurring in ,
I
the set of individual names occurring in ,
T
= 〈
T R A
〉
= 〈
S
, , , ,
H E E V
〉
a
c
is the fuzzy tableau of if (
if
)
S
is a nonempty set, (
iff
)
H
:
S
×
sub
(
K
)
→
[0,1]
maps each element
in
S
and each concept in
sub
(
to the membership degree the element belongs to the concept, (
iii
)
× × → maps each pair of elements in
S
and each role in
R
to the membership
degree the pair belongs to the role, (
iv
)
c
:
E
a
:
S S R
[0,1]
K
D
× × ∆ maps each pair of elements and
concrete values and each concrete role in
R
D
to the membership degree the pair belongs to the role, (
v
)
V
S
R
[0,1]
D
:
I
® maps each individual in
I
to a element in
S
. Additionally, for each
s
, Î
S
,
C D sub
A
,
Î ,
R
Î
R
, and
n
Î [0,1],
T
satisfies:
(
)
1.
for each s
Î
S
, ( ,
s
^ ,
H
) = 0
( ,
s
=1;
2.
if
( ,
s C D
)
³ , then ( ,
n
s C
)
³ and ( ,
s D
)
³ ;
3.
if
( ,
s C D
)
³ , then ( ,
n
s C
)
³ or ( ,
s D
)
³ ;
4.
if
( ,
s R C
∀
.
)
≥ , then for all
t
Î
S
, (
n
〈
s t R
,
〉
,
)
≤ −
1
n
or ( ,
t C
)
³ ;
5.
if
( ,
s R C
∃
.
)
≥ , then there exists
t
Î
S
, such that
a
n
(
〈
s t R
,
〉
,
)
≥ and ( ,
n
t C
)
³ ;
6.
if
( ,
s R C
∀
.
)
≥ , and Trans (
n
R
, then
a
(
〈
s t R
,
〉
,
)
≤ − or ( ,
1
n
t R C
∀
.
)
≥ ;
n
7.
if
( ,
s
∀
S C
.
)
≥ , Trans (
n
R
, and
R
*
S
, then
a
(
〈
s t R
,
〉
,
)
≤ − or ( ,
1
n
t R C
∀
.
)
≥ ;
n
8.
if
( ,
s
³ ³ , then #{
2 )
S
n
t
∈
S
|
(
〈
s t R
,
〉
,
)
≥
n
;
a
9.
if
( ,
s
≤
1 )
S
≥ , then #{
n
t
∈
S
|
(
〈
s t R
,
〉
,
)
≥ − +
1
n
ε ;
a
10.
if
a
(
〈
s t R
,
〉
,
)
≥ , and
R
n
*
S
, then
a
(
〈
s t S
,
〉
,
)
≥ ;
n
11.
a
(
〈
s t R
,
〉
,
)
≥ iff
a
n
(
〈
t s
,
〉
,
Inv R
(
))
≥ ;
n
N
q
12.
if C
D
Î , then for all
s
Î
S
,
n N
∈
∪
, ( ,
s C
¬ ≥ − + ε or ( ,
)
1
n
s D
)
³ ;
13.
if C o
( ) ≥ ∈ , then
H V
n
(
( ),
o C
)
³ ;
′
≥ ∈ , then
E V
′
〉
14.
if R o o
( ,
n
(
〈
( ),
o
V
(
o
) ,
R
)
≥ ;
n
a
≈
′
/ , then
′
.
15.
if o
( )
o
≠
(
o
)
