Information Technology Reference
InDepth 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
UIFDPLL
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
UIFDPLL
is terminating. We will prove it
in Section 4.1.
Definition 5.
ACNF
φ
is called reduced if none of the reduction rules of
UIFDPLL
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 nonpropagated clause in
φ
{{s ≈ t}}
if
s, t ∈
Term
(
φ
)
.
The set of all nonpropagated 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