Database Reference
In-Depth Information
subscripts, and the variables in
M
BD
as
y
's, possibly with subscripts. Initialize
S
AB
and
S
BD
to be the empty sets. Assume that the SOtgd in
M
AB
is
f
∀
x
1
(φ
A,
1
⇒
ψ
B,
1
)
∧···∧
∀
x
n
(φ
A,n
⇒
ψ
B,n
)
.
∃
For 1
ψ
B,i
into
S
AB
if these implications
are not ground formulas. We do likewise for
≤
i
≤
n
, put the
n
implications
φ
A,i
⇒
M
BD
and
S
BD
.If
S
AB
=∅
or
S
BD
=∅
and go to step 5.
Each implication
χ
in
S
AB
has the form
φ
A,i
(
x
i
)
then set
S
BD
={
r
∅
⇒
r
∅
}
⇒∧
1
≤
j
≤
k
r
j
(
t
j
)
where ev-
ery member of
x
i
is a universally quantified variable, and each
t
j
,for1
k
,
is a sequence (tuple) of terms over
x
i
. We then replace each such implication
χ
in
S
AB
with
k
implications
φ
A,i
(
x
i
)
≤
j
≤
⇒
r
1
(
t
1
),...,φ
A,i
(
x
i
)
⇒
r
k
(
t
k
)
.
In all implications in
S
BD
replace all equations
(f
r
i
(
t
i
)
=
1
)
with
r
i
∈
A
on
the left-hand sides by the atoms
r
i
(
t
i
)
.
2. (
Compose S
AB
with S
BD
)
Repeat the following as far as possible:
For each implication
χ
in
S
BD
of the form
ϕ
ψ
D
where there is an atom
r(
y
)
in
ϕ
, we perform the following steps to (possibly) replace
r(
y
)
with atoms over
A
⇒
. (The part of formula
ϕ
composed of built-in predicates
.
,>,<,...
is left
unchanged). Let
φ
1
⇒
r(
t
1
),...,φ
l
⇒
r(
t
l
)
be all the implications in
S
AB
whose
right-hand side is an atom with the relational symbol
r
. For each such implication
φ
i
⇒
r(
t
i
)
, rename the variables in this implication so that they do not overlap
with the variables in
χ
. (In fact, every time we compose this implication, we take
a fresh copy of the implication, with new variables.) Let
θ
i
be the conjunction
of the equalities between the variables in
r(
y
)
and the corresponding terms in
r(
t
i
)
, position by position. For example, the conjunction of equalities, position
by position, between
r(y
1
,y
2
,y
3
)
and
r(x
1
,f
2
(x
2
),f
1
(x
3
))
is
(y
1
=
,
=
.
=
.
=
x
1
)
∧
(y
2
.
=
∧
f
2
(x
2
))
(y
3
f
1
(x
3
))
. Observe that every equality that is generated has the
.
=
M
BD
and
t
is a term based on variables in
M
BD
and on functions in the tuple
f
. Remove
χ
from
S
BD
and add
l
implications
to
S
BD
as follows: replace
r(
y
)
in
χ
with
φ
i
∧
form
y
t
where
y
is a variable in
θ
i
and add the resulting implication
l
.
3. (
Remove the variables originally in
to
S
BD
,for1
≤
i
≤
M
BD
)
For each implication
χ
constructed in the previous step, perform the elimination
of the variables
y
i
from
.
=
M
BD
as far as possible: Select an equality
y
i
t
that
was generated in the previous step (thus
y
i
is a variable in
M
BD
and
t
is a term
.
=
based on variables in
M
AB
and on
f
). Remove the equality
y
i
t
from
χ
and
replace every remaining occurrence of
y
i
in
χ
by
t
.
4. (
Remove remained atoms with relational symbols in
)
For the implications in
S
BD
repeat the following, in order to eliminate all rela-
tional symbols (on the left-hand side of implications) that are not in
B
that are not in
A
:
For each
χ
in
S
BD
such that its left-hand side is equal to a conjunction
φ
1
(
x
)
(that
contains only the relational symbols in
A
and the equations with functional sym-
bols) and
φ
2
(
x
,y
1
,...,y
k
)
(with
x
a subset of
x
) that contains only the atoms
with relational symbols that are not in
A
A
, we modify
φ
2
from the left-hand side
