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

| MLit ( Core ( REDUCE ( ψ ∧ l ))) | <n ,

| MLit ( Core ( REDUCE ( ψ ∧¬l ))) | <n .

Since φ is unsatisfiable then by Lemma 18, ψ is also unsatisfiable. Then for
each l ∈ Lit , ψ ∧ l and ψ ∧¬l are unsatisfiable. By Lemma 18, REDUCE ( ψ ∧ l )
and REDUCE ( ψ ∧¬l ) are unsatisfiable. By induction hypothesis, the procedure
returns “unsatisfiable” for REDUCE ( ψ ∧ l )and REDUCE ( ψ ∧¬l ). By definition
of UIF-DPLL , the procedure returns “unsatisfiable” for φ .
( ) Let the procedure returns “unsatisfiable”. We will give a proof by in-

duction on the number of UIF-DPLL calls.
Base case . Let the procedure returns “unsatisfiable” after one call. Then
⊥∈ REDUCE ( φ ). By Lemma 18, we obtain that φ is unsatisfiable.
Inductive step .Let φ

⇐

be unsatisfiable if UIF-DPLL ( φ ) returns “unsatisfi-

1 calls. Assume that UIF-DPLL ( φ ) returns “unsatisfi-
able” after n calls. By definition of UIF-DPLL , UIF-DPLL ( REDUCE ( φ )

n −

able” after at most

∧ l )and

UIF-DPLL ( REDUCE ( φ ) ∧¬l ) returns “unsatisfiable” after at most n − 1 calls.

Then by induction hypothesis, REDUCE ( φ ) ∧¬l are unsat-

isfiable CNFs. We obtain that REDUCE ( φ ) is unsatisfiable. By Lemma 18, φ is
also unsatisfiable.

∧ l and REDUCE ( φ )

6 The Extended UIF-DPLL Calculus

In this section we will introduce an optimization technique which can be used
as a preprocessing step.

Definition 20. Let t ∈ SubTerm ( φ ) , depth ( t ) > 1 and for each s ∈ SubTerm p ( t )
and u ∈ Term ( φ ) , ( s ≈ u ) ∈ Lit ( φ ) .Then t is called reducible in φ .

Example 21. Let us consider the formula from Example 11.

¬φ 0 : u 1 ≈ f ( x 1 ,y 1 ) ∧u 2 ≈ f ( x 2 ,y 2 ) ∧z ≈ g ( u 1 ,u 2 ) ∧z ≈ g ( f ( x 1 ,y 1 ) ,f ( x 2 ,y 2 )) .

The terms f ( x 1 ,y 1 )and f ( x 2 ,y 2 ) are reducible.

Definition 22. Avariable x is called fresh in φ if x ∈ Var ( φ ) .

6.1 The Term Reduction Rule

One may add one more rule to the UIF-DPLL calculus.

φ
φ [ t := x ]

Term Reduction : if t is reducible and x is fresh in φ

This rule can be applied as a preprocessing step. We will show it with an
example.