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