Database Reference
In-Depth Information
(1) If π( )
x
∈
AfterBlocked Gi∈
i
(
)
, then
Tail
( ( )) =
p
x
Tail
'( ( ))
p . If π( )
x
x
∈
AfterBlocked Gi∈
i
(
)
, then there
exists some
y Vars q
Î ( ) , such that π(
y
)
∈
Blocked Gi∈
i
(
)
, i.e.,
Tail
( (
π
y
))
≠
Tail
'( (
π
y
))
, and p(
x
¢
¢
is a descendant of p(
y
. p(
x
is of the form [
p v
|
/
v
,
,
v
/
v
]
, where
Tail p
(
)
¹
Tail p
'(
)
.
0
0
m
m
≠
′
, then the length of the path p(
x
is larger than
k
, which contradicts with the
Assume that
v
v
m
π
π
fact that
d
( ,
x y
) ≤
d
≤ ≤ .
n
k
q
q
(2) If π( )
x
∈
V G
i
(
)
for some
G
i
with
afterblocked Gi∈
i
(
) ≠ ∅ and π( )
x
∉
afterblocked Gi∈
i
(
)
, then
Tail
'( ( )p is tree-blocked by ψ
x
(
Tail
'( ( )))
π
x
. If
afterblocked Gi∈
i
) ≠ ∅
, then there exists some
(
y Vars q
Î ( ) , such that
π(
has some proper sub-path
p
such that
Tail p
)
.
y
)
∈
Nodes G
i
(
)
(
) =
Tail p
'(
Since p(
x
and p(
y
are in the same
G
i
, then either p(
x
is an ancestor of p(
y
or there is some
z
Î
Terms q
( ) such that p(
z
is a common ancestor of p(
x
and p(
y
in
Nodes G
i
(
) . In the first
case, if
Tail
'( ( )p was not tree-blocked, we would have that
d
x
π
( ,
x y
) > ≥ , which is a contradic-
n
n
q
tion. In the second case, if
Tail
'( ( )p was not tree-blocked, then
Tail
x
'( ( )p would not be tree-blocked
z
π
( ,
either, and thus we also derive a contradiction since
d
z y
) > ≥ .
n
n
q
We thus can construct the mapping µ :
Terms q
( )
→
Nodes
(
as follows.
)
•
For each
a
Î ( ) , µ
Inds q
( ) =
a
Tail
( ( )) =
π
a
a
;
•
For each
x Vars q
Î ( ) with π( )
x
∈
afterblocked Gi∈
i
(
)
, µ
( ) =
x
Tail
( ( ))
π
x
;
◦
If
afterblocked Gi∈
i
(
) = Æ, then µ
( ) =
x
Tail
( ( ))
π
x
,
We now prove that m satisfies Property 1-3 in Definition 9.
Property 1 follows from the construction of m;
Property 2: For each fuzzy concept atom
C x
Tail
'( ( ))
π
x
if
π
( )
∈
rwise
.
x
afterblocked Gi∈
(
),
i
◦
If
afterblocked Gi∈
i
(
) ≠ ∅, then µ
( ) =
x
ψ
(
Tail
'( ( )))
π
x
othe
( ) ≥ ∈ , since I
F
n
q
q
, ( ( ),
π
x C
)
≥ holds. It follows
that 〈 ≥ 〉 ∈
C
,
,
n
(
Tail
'( ( )))
π
x
or 〈 ≥ 〉 ∈
C
,
,
n
ψ
(
(
Tail
'( ( ))))
π
x
, then we have 〈 ≥ 〉 ∈
C
,
,
n
µ
( ( ))
x
.
Property 3: For each fuzzy role atom
R x y
( ,
) ≥ ∈ , (
n
q
〈
π
( ),
x
π
(
y R
) ,
〉
)
≥
n
holds. Then, either
(1)
Tail
'( ( )p is a
R
n
y
³,
-successor of
Tail
( ( )p , or (2)
Tail
x
'( ( )p is a
Inv R
x
(
)
-successor of
³
,
n
Tail
( ( )p .
case (1): For each connected component
G
i
, if
AfterBlocked Gi∈
i
y
(
) = Æ, then for each term
x
such
that π( )
x
G
∈ ,
Tail
( ( ) =
p
x
Tail
'( ( )
p . If
Tail
x
'( ( )p is a
R
n
y
³,
-successor of
Tail
( ( )p , then
x
µ
(
y
) =
Tail
'( (
π
y
is a
R
n
))
³,
-successor of µ
( ) =
x
Tail
( ( ))
π
x
.
If
AfterBlocked Gi∈
i
(
) ≠ ∅, we make case study as follows.
(a) If π
( ),
x
π
(
y
)
∈
AfterBlocked Gi∈
i
(
)
, then µ
( ) =
x
Tail
'( ( ))
π
x
and µ
(
y
) =
Tail
'( (
π
y
. If
Tail
))
'( ( )p
y
is a
R
n
³,
-successor of
Tail
( ( )p , then µ
x
(
y
) =
Tail
'( (
π
y
is a
R
n
))
³,
-successor of
µ
( ) =
x
Tail
'( ( )) =
π
x
Tail
( ( ))
π
x
.
(b) If π
( ),
x
π
(
y
)
∉
AfterBlocked Gi∈
i
(
)
, then
Tail
'( ( )) =
p
x
Tail
( ( ))
p . Otherwise, there will be
x
π(
y
)
∈
AfterBlocked Gi∈
i
(
)
. By Property (2),
Tail
'( ( )p is tree-blocked by ψ
x
(
Tail
'( ( )))
π
x
,
