TY - GEN A1 - Richter-Gebert, Jürgen T1 - Mechanical Theorem Proving in Projective Geometry. N2 - We present an algorithm that is able to confirm projective incidence statements by carrying out calculations in the ring of all formal determinants (brackets) of a configuration. We will describe an implementation of this power and present a series of examples treated by the prover, including {\it Pappos' and Desargues' Theorems,} the {\it Sixteen Point Theorem, Saam's Theorem, }the {\it Bundle Condition,} the uniqueness of a harmonic Point and {\it Pascal's Theorem.} T3 - ZIB-Report - SC-93-05 Y1 - 1993 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:0297-zib-1013 ER -