# Author’s note to the English-language edition

## Abstract

Mechanical theorem proving (MTP) is a traditional topic of mathematical logic. In contrast to the usual approaches to MTP by mathematical logic, approaches using algebraic methods seem to be originated in the paper by the present writer (Wu 1978). In 1984 appeared the present book “Basic Principles of Mechanical Theorem Proving in Geometries” devoted to a systematic exposition of such algebraic methods for MTP. The book, written in Chinese and published in China, was little known beyond China. The method became widely known owing to papers by Wu (1978, 1984a) and Chou (1984) published in the anthology edited by Bledsoe and Loveland (1984). Since that time the algebraic methods of treating MTP have been developed rapidly and vigorously in various directions. For example, in 1986 there appeared several papers on MTP based on Gröbner basis method and others (e.g., Kutzler and Stifter 1986, Kapur 1986). In this note we shall give a brief review of the achievements of MTP in recent years restricted, however, to the methods as exhibited in the present book alone. Thus it may serve merely as complement and addendum to the original version of the book.

## Keywords

Theorem Prove Algebraic Method Present Writer Automate Theorem Prove Geometric Theorem## Preview

Unable to display preview. Download preview PDF.

## References

- Bledsoe, W. W., Loveland, D. W. (eds.) (1984): Automated theorem proving: after 25 years. American Mathematical Society, Providence.MATHCrossRefGoogle Scholar
- Chou, S. C. (1984): Proving elementary geometry theorems using Wu’s algorithm. In: Bledsoe, W. W., Loveland, D. W. (eds.): Automated theorem proving: after 25 years. American Mathematical Society, Providence, pp. 243–286.Google Scholar
- Chou, S. C. (1985): Proving and discovering geometry theorems using Wu’s method. Ph.D. Thesis, University of Texas at Austin, Austin, Texas.Google Scholar
- Chou, S. C. (1988): Mechanical geometry theorem proving. Reidel, Lancaster.MATHGoogle Scholar
- Chou, S. C., Gao, X. S. (1989a): On the mechanical proof of geometry theorems involving inequalities. University of Texas at Austin, Preprint TR-89-31.Google Scholar
- Chou, S. C., Gao, X. S. (1989b): Mechanical theorem proving in differential geometry — I. Space curves. Math. Mech. Res. Preprints 4: 109–123.Google Scholar
- Chou, S. C., Gao, X. S. (1991): Theorems proved automatically using Wu’s method — part on differential geometry (space curves) and mechanics. Math. Mech. Res. Preprints 6: 37–55.Google Scholar
- Chou, S. C., Gao, X. S. (1992): An algebraic system based on the characteristic set method. In: Proceedings IWMM’ 92, Beijing, pp. 1–18.Google Scholar
- Chou, S. C., Schelter, W. F., Yang, J. G. (1985): Characteristic sets and Gröbner bases. University of Texas at Austin, Preprint.Google Scholar
- Chou, S. C., Gao, X. S., Zhang, J. Z. (1992a): Automatic production of traditional proofs for theorems in Euclidean geometry — parts I-IV. Wichita State University, Preprints WSUCS-92-3,5-7.Google Scholar
- Chou, S. C., Gao, X. S., Zhang, J. Z. (1992b): Automated geometry theorem proving by vector calculation. Wichita State University, Preprint.Google Scholar
- Gao, X. S. (1987): Trigonometric identities and mechanical theorem proving in elementary geometries. J. Syst. Sci. Math. Sci. 7: 264–272 (in Chinese).MATHGoogle Scholar
- Gao, X. S. (1989): Mechanical theorem proving in Cayley-Klein geometries. Math. Mech. Res. Preprints 3: 39–50.Google Scholar
- Gao, X. S. (1990): Transcendental functions and mechanical theorem proving in elementary geometries. J. Automat. Reason. 6: 403–417 [also in Math. Mech. Res. Preprints 2: 37-47 (1987)].MathSciNetMATHCrossRefGoogle Scholar
- Gao, X. S., Wang, D. K. (1992): On the automatic derivation of a set of geometric formulae. Math. Mech. Res. Preprints 8: 26–37.Google Scholar
- Gao, X. S., Li, Y. L., Lin, D. D., Lu, X. S. (1992): A geometric theorem prover based on Wu’s method. In: Proceedings IWMM’ 92, Beijing, pp. 201–205.Google Scholar
- Hong, J.W. (1986): Can we prove geometry theorem by computing an example? Sci. Sin. A29: 824–834.Google Scholar
- Hu, S., Wang, D. M. (1986): Fast factorization of polynomials over rational number field or its extension fields. Kexue Tongbao 31: 150–156.Google Scholar
- Kapur, D. (1986): Using Gröbner bases to reason about geometry problems. J. Symb. Comput. 2: 399–408.MathSciNetMATHCrossRefGoogle Scholar
- Kapur, D., Mundy, J. L. (1988): Wu’s method and its applications to perspective viewing. Artif. Intell. 37: 15–36.MathSciNetMATHCrossRefGoogle Scholar
- Kutzler, B., Stifter, S. (1986): On the application of Buchberger’s algorithm to automated geometry theorem proving. J. Symb. Comput. 2: 389–397.MathSciNetMATHCrossRefGoogle Scholar
- Li, Z. M. (1991): Mechanical theorem proving of the local theory of surfaces. Math. Mech. Res. Preprints 6: 102–120.Google Scholar
- Lin, D. D., Liu, Z. J. (1992): Some results on theorem proving in finite geometry. In: Proceedings IWMM’ 92, Beijing, pp. 222–235.Google Scholar
- Shi, H. (1989): On the resultant formula for mechanical theorem proving. Math. Mech. Res. Preprints 4: 77–86.Google Scholar
- Wang, D. K. (1990): A mechanization proving of a group of space geometry problems. Math. Mech. Res. Preprints 5: 66–81.Google Scholar
- Wang, D. K. (1992): Mechanical solution of a group of space geometry problems. In: Proceedings IWMM’ 92, Beijing, pp. 236–243.Google Scholar
- Wang, D.M. (1988): Proving-by-examples method and inclusion of varieties. Kexue Tongbao 33: 2015–2018.MATHGoogle Scholar
- Wang, D. M. (1989a): A new theorem discovered by computer prover. J. Geom. 36: 173–182.MathSciNetMATHCrossRefGoogle Scholar
- Wang, D. M. (1989b): On Wu’s method for proving constructive geometric theorems. In: Proceedings IJCAI-89, Detroit, pp. 419–424 [also in Math. Mech. Res. Preprints 3: 89-101 (1989)].Google Scholar
- Wang, D. M. (1989c): A method for determining the finite basis of an ideal from its characteristic set with application to irreducible decomposition of algebraic varieties. Math. Mech. Res. Preprints 4: 124–140.Google Scholar
- Wang, D. M., Gao, X. S. (1987): Geometry theorems proved mechanically using Wu’s method-part on Euclidean geometry. Math. Mech. Res. Preprints 2: 75–106.MATHGoogle Scholar
- Wu, W.-t. (1978): On the decision problem and the mechanization of theorem-proving in elementary geometry. Sci. Sin. 21: 159–172 [also in Bledsoe, W. W., Loveland, D. W. (eds.): Automated theorem proving: after 25 years. American Mathematical Society, Providence, pp. 213-234 (1984)].MATHGoogle Scholar
- Wu, W.-t. (1982): Toward mechanization of geometry — some comments on Hilbert’s “Grundlagen der Geometrie”. Acta Math. Sci. 2: 125–138.MATHGoogle Scholar
- Wu, W.-t. (1983): Some remarks on mechanical theorem-proving in elementary geometry. Acta Math. Sci. 3: 357–360.MATHGoogle Scholar
- Wu, W.-t. (1984a): Some recent advance in mechanical theorem-proving of geometries. In: Bledsoe, W. W., Loveland, D. W. (eds.): Automated theorem proving: after 25 years. American Mathematical Society, Providence, pp. 235–242.Google Scholar
- Wu, W.-t. (1984b): Basic principles of mechanical theorem proving in elementary geometries. J. Syst. Sci. Math. Sci. 4: 207–235 [also in J. Automat. Reason. 2: 221-252 (1986)].Google Scholar
- Wu, W.-t. (1986a): On zeros of algebraic equations — an application of Ritt principle. Kexue Tongbao 31: 1–5.MATHGoogle Scholar
- Wu, W.-t. (1986b): A mechanization method of geometry and its applications — I. distances, areas and volumes. J. Syst. Sci. Math. Sci. 6: 204–216.MATHGoogle Scholar
- Wu, W.-t. (1986c): A mechanization method of geometry and its applications — I. dis tances, areas and volumes in Euclidean and non-Euclidean geometries. Kexue Tongbao 32: 436–440.Google Scholar
- Wu, W.-t. (1987a): A zero structure theorem for polynomial-equations-solving. Math. Mech. Res. Preprints 1: 2–12.Google Scholar
- Wu, W.-t. (1987b): On reducibility problem in mechanical theorem proving of elementary geometries. Chin. Q. J. Math. 2: 1–20 [also in Math. Mech. Res. Preprints 2: 18-36 (1987)].Google Scholar
- Wu, W.-t. (1988): A mechanization method of geometry and its applications — III. mechanical proving of polynomial inequalities and equations-solving. Syst. Sci. Math. Sci. 1: 1–17 [also in Math. Mech. Res. Preprints 2: 1-17 (1987)].MATHGoogle Scholar
- Wu, W.-t. (1989a): A mechanization method of geometry and its applications — IV. some theorems in planar kinematics. Syst. Sci. Math. Sci. 2: 97–109.MATHGoogle Scholar
- Wu, W.-t. (1989b): On the foundation of algebraic differential geometry. Syst. Sci. Math. Sci. 2: 289–312 [also in Math. Mech. Res. Preprints 3: 1-26 (1989)].MATHGoogle Scholar
- Wu, W.-t. (1989c): On the generic zero and Chow basis of an irreducible ascending set. Math. Mech. Res. Preprints 4: 1–21.Google Scholar
- Wu, W.-t. (1991): Mechanical theorem proving of differential geometries and some of its applications in mechanics. J. Automat. Reason. 7: 171–191 [also in Math. Mech. Res. Preprints 6: 1-22 (1991)].MathSciNetMATHGoogle Scholar
- Wu, W.-t. (1992a): A report on mechanical geometry theorem proving. Prog. Natural Sci. 2: 1–17.Google Scholar
- Wu, W.-t. (1992b): On problems involving inequalities. Math. Mech. Res. Preprints 7: 1–13.Google Scholar
- Wu, W.-t. (1992c): On a finiteness theorem about optimization problems. Math. Mech. Res. Preprints 8: 1–18.MATHGoogle Scholar
- Wu, W.-t. (1992d): A mechanization method of equations solving and theorem proving. Adv. Comput. Res. 6: 103–138.MATHGoogle Scholar
- Wu, W.-t. (1993): Mechanical theorem proving in differential geometries. In: Proceedings XXI DGM, Singapore (to appear).Google Scholar
- Wu, W.-t., Lu, X. L. (1985): Triangles with equal bisectors. People’s Education Press, Beijing (in Chinese).Google Scholar
- Yang, L., Zhang, J. Z., Li, C. Z. (1992): A prover for parallel numerical verification of a class of constructive geometry theorems. In: Proceedings IWMM’ 92, Beijing, pp. 244–250.Google Scholar