Information Technology Reference
In-Depth Information
The set of positive clauses of length more than one contained in
φ
is called
the
core
of
φ
, and it is denoted by
Core
(
φ
).
In a CNF
φ
let
-
Var
(
φ
) be the set of all constants in
φ
,
-
At
(
φ
) be the set of all atoms in
φ
,
-
Lit
(
φ
) be the set of all literals in
φ
,
-
MLit
(
φ
) be the multiset of all literals contained in
φ
,
-
Cls
(
φ
) be the set of all clauses in
φ
.
We define
Term
(
φ
)=
{t ∈
Term
|∃s ∈
Term
:(
ts
)
∈
Lit
(
φ
)
}
.
SubTerm
(
φ
)=
t∈
Term
(
φ
)
SubTerm
(
t
).
2.2
Semantics
Let
At
be a set of atoms.
We define an
interpretation
as a function
I
:
At
→{
true
,
false
}
.
A literal
l
is
true
in
I
iff either
l
is an atom
a
and
I
(
a
)=
true
or
l
is a negated
atom
=
l
, if a literal
l
is
true
in
I
.
We define an E-interpretation as one satisfying the following conditions.
¬a
and
I
(
a
)=
false
.Wewrite
I
|
-
I
=
t ≈ t
;
-
if
I
|
|
=
s ≈ t
then
I
|
=
t ≈ s
;
-
if
I
|
=
s ≈ u
and
I
|
=
u ≈ t
then
I
|
=
s ≈ t
;
-
if
I
|
=
s
i
≈ t
i
for all
i ∈{
1
,...,n}
then
I
|
=
f
(
s
1
,...,s
n
)
≈ f
(
t
1
,...,t
n
).
We write
I
|
=
φ
if a formula
φ
is
true
in
I
.
Definition 1.
Aformula
φ
is called satisfiable if
I
|
=
φ
for some E-interpretation
I
.
Otherwise
φ
is called unsatisfiable.
By definition the empty clause
⊥
is unsatisfiable.
We will use throughout the paper the following notations.
Let
s ∈
SubTerm
(
t
). Then
φ
[
t
:=
s
] denotes the formula that is obtained from
φ
by substituting recursively all occurrences of the term
t
by the term
s
till no
occurrences of
t
is left.
Example 2.
Let us consider
φ
=
{{f
(
f
(
x
))
≈ y}, {x ≈ g
(
y
)
}}
.
Then
φ
[
f
(
x
):=
x
]=
{{x ≈ y}, {x ≈ g
(
y
)
}}
.
We define
φ|
l
=
{C −{¬l}| C ∈ φ, l ∈ C}
.
Example 3.
Let us consider
φ
=
{{x ≈ f
(
y
)
,z≈ g
(
z
)
}, {x ≈ f
(
y
)
,y≈ g
(
z
)
}}
.
Then
φ|
x≈f
(
y
)
=
{{y ≈ g
(
z
)
}}
.
Search WWH ::
Custom Search