Database Reference
In-Depth Information
ψ i ( x i ))
ψ i ( x i ))
2.2. We add the implication (r q i ( y i )
r i ( t i )
if y i is empty) in S M , where ψ ( x i ) is the formula obtained from q Ai ( x i ) by
substituting each atom r( t ) in it (where t is a tu ple of terms with variables in
x i ) by a logically equivalent atom (f r ( t ) .
r i ( t i ) (or (r
f is a new fresh
introduced symbol for the characteristic function of r (hence, ψ ( x i ) ) and
q Ai ( x i ) are logically equivalent).
3. ( Construct SOtgd Φ E and Φ M )
3.1. If S M ={
=
1 ) , where f r /
and χ 1 ,...,χ m are the implications from the previous
step then Φ M is a singleton set composed of an SOtgd
χ 1 ,...,χ m }
x 1 χ 1 ∧···∧∀
h (
x m χ m )
where h
f is the tuple of all functional symbols that appear in any of the
implications in S M and the variables in x i are all the variables found in the
formula χ i , for1
i
m .
3.2. If S E ={
and χ 1 ,...,χ m are the implications from the previ-
ous step then Φ E is a singleton set composed of an SOtgd
χ 1 ,...,χ m }
g (
z 1 χ 1 ∧···∧∀
z m χ m )
where g
f is the tuple of all functional symbols that appear in any of the
implicati on s in S E and the variables in z i are all the variables found in the
formula χ i ,for1
m .
Return the pair of SOtgds M E ) .
i
It is easy to verify that for a mapping
M AB ={
Φ
}: A B
, with this de-
composition M E )
=
DeCompose(
M AB ) , we obtain two mappings,
M AC =
{
Φ E }: A C
M CB ={
Φ M }: C B
C =
) and S C is the set
of all new introduced relational symbols (that appear on the right-hand side of
implications in Φ E and on the left-hand side of implications in Φ M ), such that
M AB = M CB M AC =
and
, where
(S C ,
Compose(
M CB ,
M AC ) (from the fact that for each par of
ψ i ( x i ))
implications χ i and χ i , equal to q Ai ( x i )
r q i ( y i ) and (r q i ( y i )
r i ( t i ) ,
respectively, ψ i ( x i ) is logically equivalent to q Ai ( x i ) .
Example 16 Let us consider the following three cases:
1. The mapping
M AD ={ Φ }: A D
in Example 5 with Φ equal to SOtgd
f 1
x 2 Takes (x 1 ,x 2 )
Enrolment f 1 (x 1 ),x 2 .
x 1
Then Φ E is equal to
x 1
x 2 ( Takes (x 1 ,x 2 )
r q 1 (x 2 )) , and Φ M is equal to
f Ta k e s
x 2 r q 1 (x 2 )
f Ta k e s (x 1 ,x 2 ) .
f 1
x 1
1 Enrolment f 1 (x 1 ),x 2 ,
=
where f Ta k e s is a new functional symbol introduced in step 2 of the algorithm
DeCompose because the variable x 1 on the right-hand side of the implication is
not contained in the atom r q 1 (x 2 ) and, consequently, we replaced the original
Search WWH ::




Custom Search