Information Technology Reference
InDepth Information
mation [12] transforms an arbitrary propositional formula into a CNF in such a
way that the original formula is satisfiable if and only if the CNF is satisfiable.
Both the size of the resulting CNF and the complexity of the transformation
procedure is linear in the size of the original formula. In this transformation new
propositional variables are introduced. So applying it directly to EUF formulas
will yield a CNF in which the atoms are both equalities and propositional vari
ables. However, if we have
n
propositional variables
p
1
,...,p
n
we can introduce
n
+ 1 fresh variables
x, y
1
,...y
n
and replace every propositional variable
p
i
by
the equality
x ≈ y
i
. In this way satisfiability is easily seen to be maintained.
Hence we may and shall restrict to the satisfiability of CNFs.
2.1
Syntax
Let
Σ
=(
Fun
, ≈
) be a signature, where
Fun
=
{f,g,h,...}
is a set of
function
symbols
.
For every function symbol its
arity
is defined, being a nonnegative integer.
We assume a set
Var
=
{x,y,z,...}
of
variables
.Thesets
Var
and
Fun
are
pairwise disjoint.
The set
Term
of terms is inductively defined as follows.
• x ∈
Var
is a term,
• f
(
t
1
,...,t
n
)isatermif
t
1
,...,t
n
are terms, and
f ∈
Fun
.
Symbols
s, t, u
denote terms.
A subterm of a term
t
is called
proper
if it is distinct from
t
.Thesetof
subterms of a term
t
is denoted by
SubTerm
(
t
). The set of proper subterms of a
term
t
is denoted by
SubTerm
p
(
t
).
The
depth
of a term
t
is denoted by
depth
(
t
) and inductively defined as
follows.

depth
(
x
)=1if
x ∈
Var
,

depth
(
f
(
t
1
,...,t
n
)) = 1 + max(
depth
(
t
1
,...,t
n
)).
An
atom
a
is an equality of the form
s ≈ t
,where
s, t ∈
Term
.Weconsider
s ≈ t
t ≈ s
as the same atom. The set of atoms over the signature
Σ
and
is
denoted by
At
(
Σ,
Var
) or for simplicity by
At
.
A
literal
l
is an atom or a negated atom. We say that
l
is a
positive literal
if it is coincides with some atom
A
, otherwise it is called a
negative literal
.The
set of all literals over the signature
Σ
is denoted by
Lit
(
Σ,
Var
)orifitisnot
relevant by
Lit
.By
ts
is denoted either a literal
t ≈ s
or a literal
t ≈ s
.
A
clause
C
is a set of literals. The number of literals in a clause is called
the
length
of the clause. The clause of length 0 is called the empty clause, and
it is denoted by
. A nonempty clause
C
is called
positive
if it contains only
positive literals, otherwise it is called
negative
. The set of clauses is denoted by
Cls
. A clause is called
unit
if it contains only one literal.
A
formula
φ
is a set of clauses. The set of formulas is denoted by
Cnf
.
⊥
Search WWH ::
Custom Search