|
 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 non-trivial examples is given, based on an implementation of the methods in the computer algebra system SAC-2 on an IBM 4341.
REFERENCES
Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.
| |
1
|
Buchberger B., 1965,1970: An Algorithm for Finding a Basis for the Residue Class Ring of a Zero-Dimensional Polynomial Ideal (German). Univ. of Innsbruck, Inst. f. Mathematik, Ph.D. thesis, and Aequationes Math., eel. 4, fasc. 3, pp. 374-383, Birkh~iuser.
|
| |
2
|
Buchberger B., 1985: Gr~bner Bases - An Algorithmic Method in Polynomial Ideal Theory. Chapter 6 in N.K. Bose (ed.): 'Multidimensional Systems Theory', D.Reidel Publ. Comp.
|
| |
3
|
Chou S.C., 1984: Proving Elementary Geometry Theorems Using Wu's Algorithm. Contemporary Mathem., eel. 29, pp. 243-286.
|
| |
4
|
Chou S.C., 1985: Proving and Discovering Theorems in Elementary Geometries Using Wu's Method. Univ. of Texas, Ph.D. thesis.
|
| |
5
|
|
| |
6
|
Collins G.E., SAC-2 Manual. Univ. ofWisconsin, C.S. Dept.
|
| |
7
|
Gebauer R., Kredel H., 1984: Buchberger Algorithm System. SIGSAM Bulletin, eel. 18, no. 1, 1984.
|
| |
8
|
Gr6bner W., 1949: Modern Algebraic Geometry (German) Springer,
|
| |
9
|
Kapur D., 1986: Geometry Theorem Proving Using Gr~bner Bases. To appear as application letter in the J. of Symbolic Computation.
|
| |
10
|
|
| |
11
|
Kutzler B., Stiffer S., 1986b: Collection of Computerized Proofs of Geometry Theorems. Univ. Linz, technical report.
|
 |
12
|
|
| |
13
|
Wu W.T., 1982: Toward Mechanization of Geometry. Some Comments on Hilbert's "Grundlagen der Geometrie". Acta Mathematica Scientia, vol. 2, no. 2, pp. 125-138.
|
| |
14
|
Wu W.T., 1983: Some Remarks on Mechanical Theorem Proving in Elementary Geometry. Acta Math. Sci., vol. 3, no. 4, pp. 357-360.
|
| |
15
|
Wu W.T., 1984a: Basic Principles of Mechanical Theorem Proving in Elementary Geometries. Journal of System Sciences and Mathematical Sciences, vol. 4, no. 3, pp. 207-235.
|
| |
16
|
Wu W.T., 1978,1984b: Some Recent Advances in Mechanical Theorem Proving of Geometries. Cont. Math., vol. 29, pp. 235-241.
|
CITED BY 7
|
|
L. W. Ericson , C. K. Yap, The design of LINETOOL, a geometric editor, Proceedings of the fourth annual symposium on Computational geometry, p.83-92, June 06-08, 1988, Urbana-Champaign, Illinois, United States
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Adobe Acrobat
QuickTime
Windows Media Player
Real Player
Pdf
F.4