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