Database Reference
In-Depth Information
is not an argument of a functional symbol) in the atom
r
j
(
t
j
)
is equal to the
n
h
th
free variable in the atom
r
n
(
t
n
)
(both atoms in
e
[
(
_
)
n
/r
n
]
1
≤
n
≤
k
), we insert the set
{
as one element of
S
. At the end,
S
is the set of sets that contain the
pairs of mutually equal free variables.
An R-algebra
α
is a
mapping-interpretation
of
(j
h
,j),(n
h
,n)
}
if it is an exten-
sion of a Tarski's interpretation
I
T
(in Definition
1
, of all predicate and functional
symbols in FOL formula
Ψ
, with
I
T
M
AB
:
A
→
B
being its extension to all formulae), and if for
each
q
i
∈
MakeOperads(
M
AB
)
it satisfies the following:
1. For each relational symbol
r
i
=
A
B
=
r
∅
in
or
,
α(r
i
)
I
T
(r
i
)
.
2. We obtain a function
f
=
α(q
A,i
)
:
R
1
×···×
R
k
→
α(r
q
)
, where for each 1
≤
ar(r
i
)
i
≤
k
,
R
i
=
U
\
α(r
i
)
if the place symbol
(
_
)
i
∈
q
i
is preceded by negation
operator
¬
;
α(r
i
)
otherwise, such that for every
d
i
∈
R
i
:
f
d
1
,...,
d
k
=
g
∗
(
t
)
=
g
∗
(t
1
),...,g
∗
(t
ar(r
B
)
)
if
{
π
j
h
(
d
j
)
=
π
n
h
(
d
n
)
|{
(j
h
,j),(n
h
,n)
}∈
S
}
is true and the assignment
g
satisfies the formula
e
[
(
_
)
n
/r
n
]
1
≤
n
≤
k
;
(empty tuple) otherwise, where the as-
signment
g
:{
x
1
,...,x
m
}→
U
is defined by the tuple of values
g(x
1
),...,g(x
m
)
)
, and its extension
g
∗
to all terms is such that for any term
=
Cmp(S,
d
1
,...,
d
k
f
i
(t
1
,...,t
n
)
:
g
∗
f
i
(t
1
,...,t
n
)
=
I
T
(f
i
)
g
∗
(t
1
),...,g
∗
(t
n
)
if
n
≥
1
;
I
T
(f
i
)
otherwise
.
The algorithm
Cmp
(compacting the list of tuples by eliminating the duplicates
defined in
S
) is defined as follows:
Input.
Aset
S
of joined (equal) variables defined above, and a list of tuples
.
Initialize
d
to
d
1
. Repeat consecutively the following, for
j
d
1
,...,
d
k
=
2
,...,k
:
Let
d
j
by a tuple of values
v
1
,...,v
j
n
, then for
i
=
1
,...,j
n
repeat consecu-
tively the following:
d
=
d
&
v
i
if there does not exist an element
{
(j
h
,j),(n
h
,n)
}
in
S
such that
j
n
;
d
, otherwise.
(The operation of concatenation '&' appends the value
v
i
at the end of tuple
d
)
Output.
The tuple
Cmp(S,
≤
d
.
3.
α(r
q
)
is equal to the image of the function
f
in point 2 above.
4. The function
h
=
α(v
i
)
:
α(r
q
)
→
α(r
B
)
such that for each
b
d
1
,...,
d
k
)
=
∈
α(r
q
)
,
h(
b
)
=
b
if
b
∈
α(r
B
)
; empty tuple
otherwise.
(
_
)
n
/r
n
]
1
≤
n
≤
k
are logically
equivale
n
t, with the only difference that the atoms with characteristic functions
f
r
(
t
)
Note that the formulae
φ
Ai
(
x
)
and expression
e
[
.
=
1 in the first formula are substituted by t
he
atoms
r(
t
)
, based on the fact
that the assi
gn
ment
g
satisfi
es
r(
t
)
iff
g
∗
(f
r
(
t
))
=
f
r
(g
∗
(
t
))
=
1 (and for every as-
ar(r)
signment
g(
1
)
=
1), where
f
r
:
U
→{
0
,
1
}
is
the characteristic function of a
ar(r)
,
f
r
(
c
)
relation
α(r)
such that for each tuple
c
∈
U
=
1if
c
∈
α(r)
; 0 otherwise.
