Information Technology Reference
mation  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.
Let Σ =( Fun , ≈
) be a signature, where Fun =
is a set of function
For every function symbol its arity is defined, being a non-negative integer.
We assume a set Var =
of variables .Thesets Var and Fun are
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
is denoted by depth ( t ) and inductively defined as
- 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 Σ
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 non-empty 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 .