Advertisement

Author’s note to the English-language edition

  • Wen-tsün Wu
Part of the Texts and Monographs in Symbolic Computation book series (TEXTSMONOGR)

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 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Bledsoe, W. W., Loveland, D. W. (eds.) (1984): Automated theorem proving: after 25 years. American Mathematical Society, Providence.MATHCrossRefGoogle Scholar
  2. 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
  3. 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
  4. Chou, S. C. (1988): Mechanical geometry theorem proving. Reidel, Lancaster.MATHGoogle Scholar
  5. 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
  6. 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
  7. 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
  8. 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
  9. Chou, S. C., Schelter, W. F., Yang, J. G. (1985): Characteristic sets and Gröbner bases. University of Texas at Austin, Preprint.Google Scholar
  10. 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
  11. Chou, S. C., Gao, X. S., Zhang, J. Z. (1992b): Automated geometry theorem proving by vector calculation. Wichita State University, Preprint.Google Scholar
  12. 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
  13. Gao, X. S. (1989): Mechanical theorem proving in Cayley-Klein geometries. Math. Mech. Res. Preprints 3: 39–50.Google Scholar
  14. 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
  15. 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
  16. 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
  17. Hong, J.W. (1986): Can we prove geometry theorem by computing an example? Sci. Sin. A29: 824–834.Google Scholar
  18. 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
  19. Kapur, D. (1986): Using Gröbner bases to reason about geometry problems. J. Symb. Comput. 2: 399–408.MathSciNetMATHCrossRefGoogle Scholar
  20. Kapur, D., Mundy, J. L. (1988): Wu’s method and its applications to perspective viewing. Artif. Intell. 37: 15–36.MathSciNetMATHCrossRefGoogle Scholar
  21. 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
  22. Li, Z. M. (1991): Mechanical theorem proving of the local theory of surfaces. Math. Mech. Res. Preprints 6: 102–120.Google Scholar
  23. 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
  24. Shi, H. (1989): On the resultant formula for mechanical theorem proving. Math. Mech. Res. Preprints 4: 77–86.Google Scholar
  25. Wang, D. K. (1990): A mechanization proving of a group of space geometry problems. Math. Mech. Res. Preprints 5: 66–81.Google Scholar
  26. Wang, D. K. (1992): Mechanical solution of a group of space geometry problems. In: Proceedings IWMM’ 92, Beijing, pp. 236–243.Google Scholar
  27. Wang, D.M. (1988): Proving-by-examples method and inclusion of varieties. Kexue Tongbao 33: 2015–2018.MATHGoogle Scholar
  28. Wang, D. M. (1989a): A new theorem discovered by computer prover. J. Geom. 36: 173–182.MathSciNetMATHCrossRefGoogle Scholar
  29. 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
  30. 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
  31. 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
  32. 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
  33. Wu, W.-t. (1982): Toward mechanization of geometry — some comments on Hilbert’s “Grundlagen der Geometrie”. Acta Math. Sci. 2: 125–138.MATHGoogle Scholar
  34. Wu, W.-t. (1983): Some remarks on mechanical theorem-proving in elementary geometry. Acta Math. Sci. 3: 357–360.MATHGoogle Scholar
  35. 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
  36. 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
  37. Wu, W.-t. (1986a): On zeros of algebraic equations — an application of Ritt principle. Kexue Tongbao 31: 1–5.MATHGoogle Scholar
  38. 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
  39. 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
  40. Wu, W.-t. (1987a): A zero structure theorem for polynomial-equations-solving. Math. Mech. Res. Preprints 1: 2–12.Google Scholar
  41. 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
  42. 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
  43. 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
  44. 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
  45. 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
  46. 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
  47. Wu, W.-t. (1992a): A report on mechanical geometry theorem proving. Prog. Natural Sci. 2: 1–17.Google Scholar
  48. Wu, W.-t. (1992b): On problems involving inequalities. Math. Mech. Res. Preprints 7: 1–13.Google Scholar
  49. Wu, W.-t. (1992c): On a finiteness theorem about optimization problems. Math. Mech. Res. Preprints 8: 1–18.MATHGoogle Scholar
  50. Wu, W.-t. (1992d): A mechanization method of equations solving and theorem proving. Adv. Comput. Res. 6: 103–138.MATHGoogle Scholar
  51. Wu, W.-t. (1993): Mechanical theorem proving in differential geometries. In: Proceedings XXI DGM, Singapore (to appear).Google Scholar
  52. Wu, W.-t., Lu, X. L. (1985): Triangles with equal bisectors. People’s Education Press, Beijing (in Chinese).Google Scholar
  53. 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

Copyright information

© Springer-Verlag Wien 1994

Authors and Affiliations

  • Wen-tsün Wu
    • 1
  1. 1.Institute of Systems ScienceAcademia SinicaBeijingPeople’s Republic of China

Personalised recommendations