Information Technology Reference

In-Depth Information

ϕ
is obviously equivalent to
true
under the assumption of
Θ
. While we receive

this result in 350 ms, regular Hermitian quantifier elimination cannot eliminate

the quantifiers using 128MB.

Example 4.
(M. Paterson's problem)
Erect three similar isosceles triangles

A
1
BC
,
AB
1
C
,and
ABC
1
on the sides of a triangle
ABC
.Then
AA
1
,
BB
1

and
CC
1
are concurrent. How does the point of concurrency moves as the areas

of the three similar triangles are varied between
0
and

.
This example is actu-

ally an example for theorem finding and not only theorem proving. See Chou [19]

for a description of this problem. We get the following elimination result:

∞

Θ

≡

u
1
u
2
−

u
2
x

−

u
3
y

=0

∧

u
2
−

x

=0

∧

u
2

=0

∧

u
3
−

y

=0

∧

y

=0
,

ϕ
≡

u
1
u
2
y
+
u
1
u
3
x

2
u
1
xy
+
u
1
u
2
y

u
1
u
3
y

−

−

2
u
1
u
2
u
3
x
+2
u
1
u
2
xy

−

u
1
u
3
x
2
+
u
1
u
3
y
2

2
u
2
xy
+2
u
2
u
3
x
2

2
u
2
u
3
y
2
+2
u
3
xy
=0

−

−

−

∨

u
1
=0
.

The result is obtained in 60 ms and describes a geometric locus. If one uses non-

generic Hermitian quantifier elimination for eliminating, the result is obtained

in 2,8 seconds and consists of 295 atomic formulas.

5

Conclusions

We have presented a generic quantifier elimination method based on Hermitian

quantifier elimination. For this purpose we have analyzed where making assump-

tions on parameters may support the algorithm: We compute generic Grobner

systems instead of regular ones reducing the practical complexity of our algo-

rithm in all cases. In the special case that no equations occur in the input, we

have additionally reduced the number of recursions needed.

By example computations we have shown that our generic Hermitian quan-

tifier elimination can be successfully used for automatic theorem proving and

theorem finding. In all examples the results are considerably shorter and the

computation times are much faster than for regular Hermitian quantifier elimi-

nation.

References

1. Collins, G.E.: Quantifier elimination for the elementary theory of real closed fields

by cylindrical algebraic decomposition. In Brakhage, H., ed.: Automata Theory and

Formal Languages. 2nd GI Conference. Volume 33 of Lecture Notes in Computer

Science. Springer-Verlag, Berlin, Heidelberg, New York (1975) 134-183

2. Collins, G.E., Hong, H.: Partial cylindrical algebraic decomposition for quantifier

elimination. Journal of Symbolic Computation
12
(1991) 299-328

3. Brown, C.W.: Simplification of truth-invariant cylindrical algebraic decomposi-

tions. In Gloor, O., ed.: Proceedings of the 1998 International Symposium on

Symbolic and Algebraic Computation (ISSAC 98), Rostock, Germany, ACM, ACM

Press, New York (1998) 295-301

Search WWH ::

Custom Search