Database Reference
In-Depth Information
¢
= , we
a new node
y
is generated such that 〈 ≥ 〉 ∈ 〈
R
,
,
n
(
x y
,
〉
)
and 〈 ≥ 〉 ∈
C
,
,
n
( . By setting
y
y
o
obtain an extension of , and thus
¢ ¢
I F . The case of ³
³
-rule is analogous to the ∃
≥
-rule. The
proofs for other rules are in similar way.
Since the set of
k
-complete and clash-free completion forests for semantically captures
(modulo new individuals), we can transfer query entailment
K
q
to logical consequence of
q
from
completion forests as follows. For any completion forest and any CQ
q
, let
F
q
denote that
I
q
for every model of .
Theorem 1.
Let
k
³0 be arbitrary. Then
K
q
iff
F
q
for each Î ccf
k
(
.
)
Proof.
By Lemma 1 and Lemma 2, for each model of , there exists some
F
Î and an exten-
K
sion of , such that I F . Assume Ï ccf
k
(
, then there still have rules applicable to .
We thus obtain an expansion from and an extension
¢
of , such that
¢¢ ¢
)
I F , and so forth
until no rule is applicable. Now we either obtain a complete and clash free completion forest, or encounter
a clash. The former is conflict with the assumption, and the latter is conflict with the fact that have
models.
Checking Query Entailment Within Completion Forests
We now show that, if
k
is large enough, we can decide
F
q
for each
F
Î
ccf
k
(
)
by syntacti-
K
cally mapping the query
q
into .
Definition 9.
(Query mapping) A fuzzy query
q
can be mapped into , denoted
q
F
, if there is a
mapping
µ :
, such that (
i
) m( )
a a
, if
a
ÎInds (
q
, (
ii
) for each fuzzy concept
Terms q
( )
→
Nodes
(
)
atom
C x
( ) ³ (resp.
d x
n
( ) ³ ) in
q
,
〈
n
,
(resp. 〈
d x
( ),
≥ 〉
, ) ∈ ( ( ))
m
µ
x
with
m
³ , (
iii
)
C x
( ),
≥ 〉
m
for each fuzzy role atom
R x y
( ,
) ³ (resp.
T x y
n
( ,
) ³ ) in
q
, m(
n
y
is a
R
³
-neighbor (resp. a
T
m
³
-neighbor) of m(
x
with
m
³ .
Example 5.
By setting m( ) =
x
o
, m(
y
) =
o
, m( ) =
z
o
, and m(
y
) =
v
, we can construct a mapping
1
2
3
c
1
m of
q
into
1
.
In fact, for completion forests of a KB , syntactic mapping
q
F
implies semantic conse-
quence
F
q
.
Lemma 3.
If q
F
, then
F
q
.
Proof.
If
q
F
, then there is a mapping m : Terms(
q
® Nodes(
satisfying Definition 9. For
D of , it satisfies Definition 8. We construct a mapping p: Terms(
q
→ ∆
such that, for each term
x
Î Terms(
q
, π
.
any model
= (
,
)
x
. It satisfies
C
( ( )p =
C
(( ( )) )
( ) = ( ( ))
x
µ
x
µ
x
≥ ≥ ,
m n
( ) ≥ ∈ . The proof for fuzzy role atoms can be shown in a similar way.
Hence I
q
, which by Theorem 1 implies
F
q
.
for each fuzzy concept atom
C x
n
q
