A Decision Procedure for Equality Logic with Uninterpreted Functions - Artificial Intelligence and Symbolic Computation - page 68

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 non-negative 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 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 .

⊥