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 - TY - GEN A1 - Richter-Gebert, Jürgen A1 - Ziegler, Günter M. T1 - Zonotopal Tilings and the Bohne-Dress Theorem. N2 - We prove a natural bijection between the polytopal tilings of a zonotope $Z$ by zonotopes, and the one-element-liftings of the oriented matroid ${\cal M}(Z)$ associated with $Z$. This yields a simple proof and a strengthening of the Bohne-Dress Theorem on zonotopal tilings. T3 - ZIB-Report - SC-93-25 Y1 - 1993 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:0297-zib-1212 ER -