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

{{x ≈ y}} ∪ φ
φ [ x := y ]

Unit propagation I : if x, y ∈ Var ( φ )

{{s ≈ t}} ∪ φ
{{s ≈ t}} ∪ φ [ t := s ]

Unit propagation II : if s, t ∈ Te rm ( φ ), t ∈ SubTerm ( s )

φ
φ| t ≈ t

Tautology atom removing : if ( t ≈ t ) ∈ At ( φ )

φ

Splitting: if l ∈ Lit ( Core ( φ ))

{{l}} ∪ φ {{¬l}} ∪ φ

Fig. 1. The rules of the UIF-DPLL calculus

Definition 4. Unit propagation I, unit propagation II and tautology atom re-
moving rules are called reduction rules.

The set of reduction rules of the UIF-DPLL is terminating. We will prove it
in Section 4.1.

Definition 5. ACNF φ is called reduced if none of the reduction rules of
UIF-DPLL calculus is applicable.

4.1 Termination of the Set of Reduction Rules

We will use the notation for disjoint union , i.e., when we write φ ψ we are

referring to the union φ ∪ ψ and also asserting that φ ∩ ψ =

∅ .

Definition 6. Aunitclause {s ≈ t} is called a non-propagated clause in φ

{{s ≈ t}} if s, t ∈ Term ( φ ) .

The set of all non-propagated clauses in φ is denoted by NPCls ( φ ) .

Example 7. Let us consider the formula

φ : 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 )) .

Onecanseethat

NPCls ( ¬φ )= {{u 1 ≈ f ( x 1 ,y 1 ) }, {u 2 ≈ f ( x 2 ,y 2 ) }}.

For each ψ ∈ Cnf we define k ( φ )= | Term ( φ ) | + | MLit ( φ ) | .

Definition 8. We define a total order ≺ 1 and a total order ≺ 2 on CNFs as

follows.

φ ≺ 1 ψ if k ( φ ) <k ( ψ ) .

φ ≺ 2 ψ if NPCls ( φ ) < NPCls ( ψ ) .