Mechanical Theorem Proving in Projective Geometry.
Please always quote using this URN: urn:nbn:de:0297-zib-1013
- 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.}
Author: | Jürgen Richter-Gebert |
---|---|
Document Type: | ZIB-Report |
Date of first Publication: | 1993/02/17 |
Series (Serial Number): | ZIB-Report (SC-93-05) |
ZIB-Reportnumber: | SC-93-05 |
Published in: | Appeared in: Ann. Math. Artif. Intell. 13, No. 1-2 (1995) pp. 139-172 |