Information Technology Reference
In-Depth Information
C
D
C
O
E
A
B
F
A
B
Fig. 1.
Example 1 (left) and Example 2 (right)
For our generic type formula computation we cannot make use of our as-
sumption for computing
τ
d
.IfVar(
c
0
)
⊆{
v
1
,...,v
m
}
we can however avoid the
recursion by adding
c
0
=0to
Θ
. This reduces the size of the output formula dra-
matically and if it occurs in the recursions it reduces the computation time, too.
Our test computations have, however, shown that, in general, the assumptions
made here are very complex and cannot be easily interpreted. For our application
of automated theorem proving we have thus not analyzed this method further.
This does not mean that generic type formulas are an irrelevant optimization
for other application areas of generic quantifier elimination.
4Examp s
In this section we will apply our elimination algorithm to some automatic proofs
of geometric theorems. We have implemented the algorithm in redlog 3.0,
which is part of the current version 3.8 of the computer algebra system reduce.
For the geometric theorem proving we proceed here as described in [13].
Our examples will show the meaning of the assumptions which are created dur-
ing the computations. In most cases, these assumptions can be interpreted as
(necessary) non-degeneracy conditions, so they have a powerful geometric inter-
pretation. Note that the constructed assumptions may not be a complete list of
non-degeneracy conditions for the particular example. We will also show that
generic Hermitian quantifier elimination will speed up the elimination procedure
and will create smaller solution formulas than the regular Hermitian quanti-
fier elimination. We explain in detail how to express a geometric theorem as a
first-order formula by means of our first example.
Example 1.
Given a parallelogram
ABCD
,let
E
be the intersection point of its
diagonals. Then
E
is the midpoint of the diagonals (see Figure 1). This example
was taken from [19]. By a suitable motion in
2
we can assume w.l.o.g.
R
A
=(0
,
0)
,
B
=(
u
1
,
0)
,
C
=(
u
2
,u
3
)
,
D
=(
x
2
,x
1
)
,
E
=(
x
4
,x
3
)
.
Search WWH ::
Custom Search