Home | Quick Search | Advanced Search | Bibliography submission | Bibliography submission using bibtex | Bibliography submission using bibtex file | Links | Help | Internal


TitleAutomated geometry theorem proving using Buchberger's algorithm
Author(s) Bernhard Kutzler, Sabine Stifter
TextProceedings of the 5th ACM Symposium on Symbolic and Algebraic Computation, Waterloo, Ontario, Canada.
TypeArticle in Conference Proceedings
AbstractRecently, 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 non-trivial examples is given, based on an implementation of the methods in the computer algebra system SAC-2 on an IBM 4341.
URL http://doi.acm.org/10.1145/32439.32480
PublisherACM Press
AddressNew York, NY, USA
Translation No
Refereed No
Organization Johannes Kepler University Linz
ConferencenameSymposium on Symbolic and Algebraic Manipulation