Information Technology Reference

In-Depth Information

elimination. For this automatic solution he has used all three quantifier elimina-

tion methods, namely quantifier elimination by virtual substitution, Hermitian

quantifier elimination, and quantifier elimination by partial cylindrical algebraic

decomposition as well as the simplification methods described in [11].

The definition, development and implementation of new paradigms related to

quantifier elimination algorithms have been very successful in the past. Extended

quantifier elimination provides not only an equivalent formula but sample solu-

tions. It can be applied e.g. in the area of generalized constraint solving yielding

optimal solutions [12].

Generic quantifier elimination was introduced for the virtual substitution

method by the first author together with Sturm and Weispfenning [13]. Let
ϕ
be

an input formula with quantified variables
x
1
,...,
x
n
and parameters
u
1
,...,
u
m
.

Recall that regular quantifier elimination computes from
ϕ
aquantifier-freefor-

mula
ϕ
such that for all real values
c
1
, ...,
c
m
for the parameters
u
1
, ...,
u
m

both
ϕ
and
ϕ

ϕ
(
c
1
,...,c
m
). In

the case of generic quantifier elimination we compute additionally a conjunction

Θ
of non-trivial negated-equations, such that

are equivalent, i.e we have
ϕ
(
c
1
,...,c
m
)

←→

ϕ
)
.

In other words,
Θ
restricts the parameter space. Note that
Θ
cannot become

inconsistent, and moreover, the complement of the set described by
Θ
has a lower

dimension than the complete parameter space. Thus it restricts our parameter

space only slightly.

The idea behind the generic quantifier elimination is to add assumptions to

Θ
whenever this may either speed up the computation or may cause the algo-

rithm to produce a shorter result formula
ϕ
. The paradigm of generic quantifier

elimination was introduced in [13] in the area of automated geometry proving.

The key idea here is to express a geometric theorem as a quantified formula

and then verify it by quantifier elimination. Regular quantifier elimination may

fail due to lack of resources or if the theorem does not hold. In the latter case

it may be false only for some degenerated situations, as for empty triangles

or rectangles instead of arbitrary triangles. Generic quantifier elimination is in

this area superior to the regular one for two reasons: The computations are in

general much faster and the assumptions made in
Θ
may exclude degenerated

situations in which the theorem is false. In the above cited paper, which is based

on quantifier elimination by virtual substitution, it was heuristically shown that

for this generic quantifier elimination in fact
Θ
contains mostly non-degeneracy

conditions.

Meanwhile, using a generic projection operator, the concept of generic quan-

tifier elimination was also successfully applied to quantifier elimination by partial

cylindrical algebraic decomposition [14]. Seidl and Sturm study the general ap-

plicability of generic quantifier elimination in contrast to the regular one. As for

regular quantifier elimination by cylindrical algebraic decomposition, this ap-

proach is successful mostly for problems containing only a few variables. This

restricts the applicability of the generic projection operator to the area of auto-

mated theorem proving.

Θ

−→

(
ϕ

←→

Search WWH ::

Custom Search