Careful algebraic translations of geometry theorems

ABSTRACT

Modern application areas like computer-aided design and robotics have revived interest in geometry. The algorithmic techniques of computer algebra are important tools for solving large classes of nonlinear geometric problems. However, their application requires a translation of geometric problems into algebraic form. So far, this algebraization process has not gained special attention, since it was considered “obvious”. In the context of automated geometry theorem proving, the use of algebraic deduction techniques lead to very promising results, but it seemed to change the nature of proof problems from deciding the validity of a theorem to finding nondegeneracy conditions under which the theorem holds. A careful analysis shows, that this is mainly due to the “careless” translation method. A careful translation technique is presented that resolves this defect. The usefulness of the new algebraization method is demonstrated on concrete examples, a practical comparison with the former “careless” translation is done. Keywords: computational analytical geometry, automated geometry theorem proving.

REFERENCES

• 1: Chou, S.C. 198.5. Proving and discovering geomegrv theorems using i4ru's algorithm. PhD thesis, Univ. Texal at Austin, USA, 78 p.
• 2: Chou, S.C. 1986. A collection of geometry theorems proved mechanically. Institate for Computing Science Tech. Rep. I986- 50, Univ. Texas at Austin, USA, 142 p.
• 3: S.-C. Chou, Mechanical geometry theorem proving, Kluwer Academic Publishers, Norwell, MA, 1987
• 4: Hilbert, D. t899. Grundlagen der Geometric (The Foundations of Geometrlt}. Leipzig; also: Teubner, Stuttgart, 12th edition (xs??), ~?l p.
• 5: Deepak Kapur, Using Gro¨bner bases to reason about geometry problems, Journal of Symbolic Computation, v.2 n.4, p.399-408, Dec. 1986 [doi>10.1006/jsco.1995.1056]
• 6: K. Kusche , B. Kutzler , H. Mayr, Implementation of a geometry theorem proving package in SCRATCHPAD II, Proceedings of the European Conference on Computer Algebra, p.246-257, June 02-05, 1987
• 7: B. Kutzler , S. Stifter, On the application of Buchberger's algorithm to automated geometry theorem proving, Journal of Symbolic Computation, v.2 n.4, p.389-397, Dec. 1986 [doi>10.1016/S0747-7171(86)80006-2]
• 8: Kutzler, B., Stiffer, S. 1986b. Collection of computerized proofs of geometry theorems. Research Institute for S~lmbolic Computation Tech. tlep. 86.1~, Univ. Linz, Austria
• 9: Kutzler, B. 1988. Algebraic approaches to automated geometrg theorem pro~ing. PhD thesis, Univ. Lin~., Austria, 161p.
• 10: Shoenfield, J.R. 19(57. Mathematical Logic. Addison-Wesley Publ., Reading, 344 p.
• 11: Neil L. White , Tim McMillan, Cayley Factorization, Proceedings of the International Symposium ISSAC'88 on Symbolic and Algebraic Computation, p.521-533, July 04-08, 1988
• 12: Wu, W.T. 1978. On the decision problem and the mechanization of theorem-proving in elementary geometry. Scientia $inica, vol. 21, pp. 159-172; also: Contemporar~l }~{athematics, vol. 29 (1984), pp, 213-234
• 13: Wu, W.T. 1984. Basic principles of mechanical theorem proving in elementary geometries. J. Systems Sciences and Mathematical Sciences, vol. 4, pp. 207-235.

INDEX TERMS

Primary Classification:
  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE

Additional Classification:
  G. Mathematics of Computing
  G.2 DISCRETE MATHEMATICS

General Terms:
Algorithms, Experimentation, Theory