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