Information Technology Reference
In-Depth Information
{{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 ( ψ ) .
Search WWH ::

Custom Search