Information Technology Reference
In-Depth Information
function
check fol
(
φ
0
:
first-order formula
)
1
φ
0
←− innermost univ
(
top ex
(
φ
0
))
2(
φ
g
,∆
)
←−
abs univ
(
φ
0
)
3
return
check ground
(
φ
g
)
end
function
check comb
(
EqCls
:
set of clauses
,
PA
:
first-order theory
,
β
:
conjunction of ground literals
)
1
β
1
,β
2
)
←− purify
(
β
)
2
repeat
3
α ←−
pick an arrangement for
β
1
and
β
2
4 (
ρ
e
,ξ
e
)
←− check assign
(
EqCls,β
1
∪ α
)
5
ρ
a
←− check assign
(
PA,β
2
∪ α ∪ ξ
e
)
6
if
(
ρ
e
=
sat
)
∧
(
ρ
a
=
sat
)
then return
sat
7
until
all possible
α
's have been considered
8
return
unsat
end
Fig. 2.
A refutation-based algorithm for
non-ground
formulae
since the proof obligations arising in such a context frequently contain quanti-
fied variables, whose instantiation requires some ingenuity. In order to overcome
this diculty, we propose the algorithm
check fol
in Figure 2, which augments
check ground
with the capability of handling quantifiers. Let
φ
0
be a non-ground
formula to be checked for unsatisfiability modulo
is a finite
set of equational clauses. First, we move the existential quantifiers not in the
scope of a universal quantification to the top-most position in the formula, by
using obvious rules such as
ET ∪PA
,where
ET
∃x.P
x
∨∃x.Q
x
∃x, y.
P
x
∨Q
y
)) (cf.
top ex
, line 1). Afterwards, we minimize the scope of the remaining quantifiers
by using the rules for antiprenexing of [9] (cf.
innermost univ
, line 1). For exam-
ple, the formula
(
)
(
)rewritesto
(
(
)
(
∀x.∃y.
(
P
(
x
)
∧Q
(
y
)) is transformed to (
∀x.P
(
x
))
∧Q
(
c
y
), where
φ
0
intoaground
c
y
is a Skolem constant. Afterwards, we transform the formula
φ
0
with fresh proposi-
tional letters and recording the association between propositional letters and the
quantified sub-formulae in a mapping
formula
φ
g
by replacing the quantified sub-formulae of
φ
0
,
δ
(cf.
abs univ
, line 2) s.t.
∆
(
φ
g
)=
where
φ
g
over the Boolean con-
nectives. Then, we invoke the function
check ground
, which is a modified version
of
check ground
where the call to
check assign
(at line 5 in Figure 1) is replaced
by the following invocation of
check comb
(cf. Figure 2):
∆
denotes the homomorphic extension of
δ
to
ˆ
5
β
p
)
β
p
)),
ρ ←−
check comb
(
ET ∪
δ
(
, PA,
prop2gfol
(
where the function
ˆ
is s.t.
ˆ
δ
δ
(
β
)=
{δ
(
λ
)
| λ ∈ β
and is in the domain of
δ}
,
for any set
is imple-
mented by using a superposition prover as described in [1] and it is also capable
of returning the ground facts which are derived by the prover (cf.
β
of ground literals. We assume that
check assign
for
ET
ξ
e
at line
4of
check comb
, Figure 2). The main difference between
check comb
and the
Nelson-Oppen combination schema is that the two component procedures com-
Search WWH ::
Custom Search