Details:
Title  Automated geometry theorem proving using Buchberger's algorithm  Author(s)  Bernhard Kutzler, Sabine Stifter  Text  Proceedings of the 5th ACM Symposium on Symbolic and Algebraic Computation, Waterloo, Ontario, Canada.  Type  Article in Conference Proceedings  Abstract  Recently, geometry theorem proving has become an important topic of research in symbolic computation. In this paper we present a new approach to automated geometry theorem proving that is based on Buchberger's Gröbner bases method, one of the most important general purpose methods in computer algebra. The goal is to automatically prove geometry theorems whose hypotheses and conjecture can be expressed algebraically, i.e. in form of polynomial equations. After shortly reviewing the basic notions of Gröbner bases and discussing some new aspects on confirming theorems, we describe two different methods for applying Buchberger's algorithm to geometry theorem proving, each of them being more efficient than the other on a certain class of problems. The second method requires a new notion of reduction, which we call pseudoreduction. This pseudoreduction yields results on polynomials over some rational function field by computations that are done merely over the rationals and, therefore, is of general interest. Finally, a computing time statistics on about 40 nontrivial examples is given, based on an implementation of the methods in the computer algebra system SAC2 on an IBM 4341.  ISBN  0897911997 
URL 
http://doi.acm.org/10.1145/32439.32480 
Language  English  Pages  209214  Publisher  ACM Press  Address  New York, NY, USA  Year  1986  Translation 
No  Refereed 
No  Organization 
Johannes Kepler University Linz  Conferencename  Symposium on Symbolic and Algebraic Manipulation 
