Skip to main content
SpringerLink
Log in

Geometry machines: From AI to SMC

  • Conference paper
  • First Online:
Artificial Intelligence and Symbolic Mathematical Computation (AISMC 1996)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1138))

Abstract

The existing techniques and software tools for automated geometry theorem proving (GTP) are examined and reviewed. The underlying ideas of various approaches are explained with a set of selected examples. Comments and analyses are provided to illustrate the encouraging success of GTP which interrelates AI and SMC. We also present some technological applications of GTP and discuss its challenges ahead.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Anderson, J. R.: Tuning of search of the problem space for geometry proofs. In: Proc. IJCAI '81 (Vancouver, August 24–28, 1981), pp. 165–170.

    Google Scholar 

  2. Anderson, J. R., Boyle, C. F., Yost, G.: The geometry tutor. In: Proc. IJCAI '85 (Los Angeles, August 18–23, 1985), pp. 1–7.

    Google Scholar 

  3. Arnon, D. S.: Geometric reasoning with logic and algebra. Artif. Intell. 37: 37–60 (1988).

    Article  Google Scholar 

  4. Balbiani, P.: Equation solving in projective planes and planar ternary rings. In: LNCS 850, pp. 95–113 (1994).

    Google Scholar 

  5. Balbiani, P.: Equation solving in geometrical theories. In: LNCS 968, pp. 31–55 (1995).

    Google Scholar 

  6. Balbiani, P., Dugat, V., Fariñas del Cerro, L., Lopez, A.: Eléments de géométrie mécanique. Hermès, Paris (1994).

    Google Scholar 

  7. Balbiani, P., Fariñas del Cerro, L.: Affine geometry of collinearity and conditional term rewriting. In: LNCS 909, pp. 196–213 (1995).

    Google Scholar 

  8. Balbiani, P., Lopez, A.: Simplification des figures de la géométrie affine plane d'incidence. In: 9e congrès reconnaissance des formes et intell. artif. (Paris, January 11–14, 1994), pp. 341–351.

    Google Scholar 

  9. Bledsoe, W. W., Loveland, D. W. (eds.): Automated theorem proving: After 25 years. Comptemp. Math. 29, Amer. Math. Soc., Providence (1984).

    Google Scholar 

  10. Boissonnat, J.-D., Laumond, J.-P. (eds.): Geometry and robotics. Springer, Berlin-Heidelberg (1988).

    Google Scholar 

  11. Brüderlin, B.: Automatizing geometric proofs and constructions. In: LNCS 333, pp. 232–252 (1988).

    Google Scholar 

  12. Buchberger, B.: Gröbner bases: An algorithmic method in polynomial ideal theory. In: Multidimensional systems theory (Bose, N. K., ed.), Reidel, Dordrecht-Boston, pp. 184–232 (1985).

    Google Scholar 

  13. Buchberger, B.: Applications of Gröbner bases in non-linear computational geometry. In: Mathematical aspects of scientific software (Rice, J. R., ed.), Springer, New York, pp. 59–87 (1987).

    Google Scholar 

  14. Buchberger, B., Collins, G. E., Kutzler, B.: Algebraic methods for geometric reasoning. Ann. Rev. Comput. Sci. 3: 85–119 (1988).

    Google Scholar 

  15. Caferra, R., Herment, M.: A generic graphic framework for combining inference tools and editing proofs and formulae. JSC 19: 217–243 (1995).

    Google Scholar 

  16. Carrà Ferro, G., Gallo, G.: A procedure to prove statements in differential geometry. JAR 6: 203–209 (1990).

    Google Scholar 

  17. Carrà Ferro, G.: An extension of a procedure to prove statements in differential geometry. JAR 12: 351–358 (1994).

    Google Scholar 

  18. Cerutti, E., Davis, P. J.: Formac meets Pappus: Some observations on elementary analytic geometry by computer. Amer. Math. Monthly 76: 895–905 (1969).

    Google Scholar 

  19. Chou, S.-C.: Proving elementary geometry theorems using Wu's algorithm. In [9], pp. 243–286 (1984).

    Google Scholar 

  20. Chou, S.-C.: GEO-prover — A geometry theorem prover developed at UT. In: LNCS 230, pp. 679–680 (1986).

    Google Scholar 

  21. Chou, S.-C.: A method for the mechanical derivation of formulas in elementary geometry. JAR 3: 291–299 (1987).

    Google Scholar 

  22. Chou, S.-C.: Mechanical geometry theorem proving. Reidel, Dordrecht-Boston (1988).

    Google Scholar 

  23. Chou, S.-C.: Automated reasoning in geometries using the characteristic set method and Gröbner basis method. In: Proc. ISSAC '90 (Tokyo, August 20–24, 1990), pp. 255–260.

    Google Scholar 

  24. Chou, S.-C.: A geometry theorem prover for Macintoshes. In: LNCS 607, pp. 687–690 (1992).

    Google Scholar 

  25. Chou, S.-C., Gao, X.-S.: Mechanical formula derivation in elementary geometries. In: Proc. ISSAC '90 (Tokyo, August 20–24, 1990), pp. 265–270.

    Google Scholar 

  26. Chou, S.-C., Gao, X.-S.: Ritt-Wu's decomposition algorithm and geometry theorem proving. In: LNCS 449, pp. 207–220 (1990).

    Google Scholar 

  27. Chou, S.-C., Gao, X.-S.: Proving geometry statements of constructive type. In: LNCS 607, pp. 20–34 (1992).

    Google Scholar 

  28. Chou, S.-C., Gao, X.-S.: Automated reasoning in differential geometry and mechanics using characteristic method III. In: Automated reasoning (Shi, Z., ed.), Elsevier, North-Holland, pp. 1–12 (1992).

    Google Scholar 

  29. Chou, S.-C., Gao, X.-S.: Automated reasoning in differential geometry and mechanics using the characteristic set method — Parts I, II. JAR 10: 161–189 (1993).

    Google Scholar 

  30. Chou, S.-C., Gao, X.-S.: Automated reasoning in differential geometry and mechanics using the characteristic method IV. SSMS 6: 186–192 (1993).

    Google Scholar 

  31. Chou, S.-C., Gao, X.-S., Arnon, D. S.: On the mechanical proof of geometry theorems involving inequalities. In: Issues in robotics and nonlinear geometry (Hoffmann, C., ed.), JAI Press, Greenwich, pp. 139–181 (1992).

    Google Scholar 

  32. Chou, S.-C., Gao, X.-S., Yang, L., Zhang, J.-Z.: Automated production of readable proofs for theorems in non-Euclidean geometries. Tech. Rep. TR-WSU-94-9, Wichita State Univ., USA (1994).

    Google Scholar 

  33. Chou, S.-C., Gao, X.-S., Zhang, J.-Z.: Automated production of traditional proofs for constructive geometry theorems. In: Proc. 8th IEEE Symp. LICS (Montreal, June 19–23, 1993), pp. 48–56.

    Google Scholar 

  34. Chou, S.-C., Gao, X.-S., Zhang, J.-Z.: Automated geometry theorem proving by vector calculation. In: Proc. ISSAC '93 (Kiev, July 6–8, 1993), pp. 284–291.

    Google Scholar 

  35. Chou, S.-C., Gao, X.-S., Zhang, J.-Z.: Machine proofs in geometry. World Scientific, Singapore (1994).

    Google Scholar 

  36. Chou, S.-C., Gao, X.-S., Zhang, J.-Z.: Automated production of traditional proofs in solid geometry. JAR 14: 257–291 (1995).

    Google Scholar 

  37. Chou, S.-C., Ko, H.-P.: On mechanical theorem proving in Minkowskian plane geometry. In: Proc. IEEE Symp. LICS (Cambridge, June 16–18, 1986), pp. 187–192.

    Google Scholar 

  38. Chou, S.-C., Schelter, W. F.: Proving geometry theorems with rewrite rules. JAR 2: 253–273 (1986).

    Google Scholar 

  39. Chou, S.-C., Schelter, W. F., Yang, J.-G.: Characteristic sets and Gröbner bases in geometry theorem proving. In: Resolution of equations in algebraic structures (Aït-Kaaci, H., Nivat, M., eds.), Academic Press, San Diego, pp. 33–92 (1989).

    Google Scholar 

  40. Chou, S.-C., Schelter, W. F., Yang, J.-G.: An algorithm for constructing Gröbner bases from characteristic sets and its application to geometry. Algorithmica 5: 147–154 (1990).

    Google Scholar 

  41. Chou, S.-C., Yang, J. G.: On the algebraic formulation of certain geometry statements and mechanical geometry theorem proving. Algorithmica 4: 237–262 (1989).

    Google Scholar 

  42. Coelho, H., Pereira, L. M.: GEOM: A Prolog geometry theorem prover. Laboratório Nacional de Engenhaaria Civil Memória no. 525, Ministerio de Habitacao e Obrass Publicas, Portugal (1979).

    Google Scholar 

  43. Coelho, H., Pereira, L. M.: Automated reasoning in geometry theorem proving with Prolog. JAR 2: 329–390 (1986).

    Google Scholar 

  44. Collins, G. E.: Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In: LNCS 33, pp. 134–165 (1975).

    Google Scholar 

  45. Conti, P., Traverso, C.: A case of automatic theorem proving in Euclidean geometry: The Maclane 83 theorem. In: LNCS 948, pp. 183–193 (1995).

    Google Scholar 

  46. Crapo, H. (ed.): Computer-aided geometric reasoning. Proc. INRIA Workshop (INRIA Sophia-Antipolis, June 22–26, 1987), INRIA Rocquencourt, France.

    Google Scholar 

  47. Cyrluk, D. A., Harris, R. M., Kapur, D.: GEOMETER: A theorem prover for algebraic geometry. In: LNCS 310, pp. 770–771 (1988).

    Google Scholar 

  48. Deguchi, K.: An algebraic framework for fusing geometric constraints of vision and range sensor data. In: Proc. IEEE Int. Conf. MFI '94 (Las Vegas, October 2–5, 1994), pp. 329–336.

    Google Scholar 

  49. Deng, M.-K.: The parallel numerical method of proving the constructive geometric theorem. Chinese Sci. Bull. 34: 1066–1070 (1989).

    Google Scholar 

  50. Elcock, E. W.: Representation of knowledge in a geometry machine. Machine Intell. 8: 11–29 (1977).

    Google Scholar 

  51. Fearnley-Sander, D.: The idea of a diagram. In: Resolution of equations in algebraic structures (Aït-Kaaci, H., Nivat, M., eds.), Academic Press, San Diego, pp. 27–150 (1989).

    Google Scholar 

  52. Fevre, S.: A hybrid method for proving theorems in elementary geometry. In: Proc. ASCM '95 (Beijing, August 18–20, 1995), pp. 113–123.

    Google Scholar 

  53. Gao, X.-S.: Transcendental functions and mechanical theorem proving in elementary geometries. JAR 6: 403–417 (1990).

    Google Scholar 

  54. Gao, X.-S.: Transformation theorems among Cayley-Klein geometries. SSMS 5: 263–273 (1992).

    Google Scholar 

  55. Gao, X.-S., Chou, S.-C.: Computations with parametric equations. In: Proc. ISSAC '91 (Bonn, July 15–17, 1991), pp. 122–127.

    Google Scholar 

  56. Gao, X.-S., Li, Y.-L., Lin, D.-D., Lü, X.-S.: A geometric theorem prover based on Wu's method. In: Proc. IWMM '92 (Beijing, July 16–18, 1992), pp. 201–205.

    Google Scholar 

  57. Gao, X.-S., Wang, D.-K.: On the automatic derivation of a set of geometric formulae. J. Geom. 53: 79–88 (1995).

    Google Scholar 

  58. Gelernter, H.: Realization of a geometry theorem proving machine. In: Proc. Int. Conf. Info. Process. (Paris, June 15–20, 1959), pp. 273–282.

    Google Scholar 

  59. Gelernter, H., Hansen, J. R., Loveland, D. W.: Empirical explorations of the geometry-theorem proving machine. In: Proc. Western Joint Comput. Conf. (San Francisco, May 3–5, 1960), pp. 143–147.

    Google Scholar 

  60. Gilmore, P. C.: An examination of the geometry theorem machine. Artif. Intell. 1: 171–187 (1970).

    Google Scholar 

  61. Goldstein, I.: Elementary geometry theorem proving. MIT AI Memo no. 28, MIT, USA (1973).

    Google Scholar 

  62. Guergueb, A., Mainguené, J., Roy, M.-F.: Examples of automatic theorem proving in real geometry. In: Proc. ISSAC '94 (Oxford, July 20–22, 1994), pp. 20–24.

    Google Scholar 

  63. Hadzikadic, M., Lichtenberger, F., Yun, D. Y. Y.: An application of knowledge-base technology in education: A geometry theorem prover. In: Proc. SYMSAC '86 (Waterloo, July 21–23, 1986), pp. 141–147.

    Google Scholar 

  64. Havel, T. F.: Some examples of the use of distances as coordinates for Euclidean geometry. JSC 11: 579–593 (1991).

    Google Scholar 

  65. Hilbert, D.: Grundlagen der Geometrie. Teubner, Stuttgart (1899).

    Google Scholar 

  66. Hong, H., Wang, D., Winkler, F. (eds.): Algebraic approaches to geometric reasoning. Special issue of Ann. Math. Artif. Intell. 13(1,2), Baltzer, Basel (1995).

    Google Scholar 

  67. Hong, J.: Can we prove geometry theorems by computing an example? Sci. Sinica 29: 824–834 (1986).

    Google Scholar 

  68. Hong, J.: Proving by example and gap theorems. In: Proc. 27th Ann. Symp. Foundations Comput. Sci. (Toronto, October 27–29, 1986), pp. 107–116.

    Google Scholar 

  69. Hussain, M. A., Drew, M. A., Noble, B.: Using a computer for automatic proving of geometric theorems. Comput. Mech. Eng. 5: 56–69 (1986).

    Google Scholar 

  70. Kalkbrener, M.: A generalized Euclidean algorithm for geometry theorem proving. In [66]: 73–95 (1995).

    Google Scholar 

  71. Kandri-Rody, A., Weispfenning, V.: Non-commutative Gröbner bases in algebras of solvable type. JSC 9: 1–26 (1990).

    Google Scholar 

  72. Kapur, D.: Geometry theorem proving using Hilbert's Nullstellensatz. In: Proc. SYMSAC '86 (Waterloo, July 21–23, 1986), pp. 202–208.

    Google Scholar 

  73. Kapur, D.: Using Gröbner bases to reason about geometry problems. JSC 2: 399–408 (1986).

    Google Scholar 

  74. Kapur, D.: A refutational approach to geometry theorem proving. Artif. Intell. 37: 61–93 (1988).

    Google Scholar 

  75. Kapur, D., Mundy, J. L.: Wu's method and its application to perspective viewing. Artif. Intell. 37: 15–26 (1988).

    Google Scholar 

  76. Kapur, D., Mundy, J. L. (eds.): Geometric reasoning. Special issue of Artif. Intell. 37, The MIT Press, Cambridge (1989).

    Google Scholar 

  77. Kapur, D., Saxena, T., Yang, L.: Algebraic and geometric reasoning using Dixon resultants. In: Proc. ISSAC '94 (Oxford, July 20–22, 1994), pp. 99–107.

    Google Scholar 

  78. Kapur, D., Wan, H. K.: Refutational proofs of geometry theorems via characteristic set computation. In: Proc. ISSAC '90 (Tokyo, August 20–24, 1990), pp. 277–284.

    Google Scholar 

  79. Kelanic, T. J.: Theorem-proving with EUCLID. Creative Comput. 4/4: 60–63 (1978).

    Google Scholar 

  80. Ko, H.-P.: ALGE-prover II: A new edition of ALGE-prover. Tech. Rep. 86CRD-081, General Electric Co., Schenectady, USA (1986).

    Google Scholar 

  81. Ko, H.-P.: Geometry theorem proving by decomposition of quasi-algebraic sets: An application of the Ritt-Wu principle. Artif. Intell. 37: 95–122 (1988).

    Google Scholar 

  82. Ko, H.-P., Chou, S.-C.: A decision method for certain algebraic geometry problems. Rocky Mountain J. Math. 19: 709–724 (1989).

    Google Scholar 

  83. Ko, H.-P., Hussain, M. A.: A study of Wu's method — A method to prove certain theorems in elementary geometry. Congr. Numer. 48: 225–242 (1985).

    Google Scholar 

  84. Ko, H.-P., Hussain, M. A.: ALGE-prover: An algebraic geometry theorem proving software. Tech. Rep. 85CRD139, General Electric Co., Schenectady, USA (1985).

    Google Scholar 

  85. Kusche, K., Kutzler, B., Stifter, S.: Implementation of a geometry theorem proving package in Scratchpad II. In: LNCS 387, pp. 246–257 (1989).

    Google Scholar 

  86. Kutzler, B.: Algebraic approaches to automated geometry theorem proving. Ph.D thesis, RISC-LINZ, Johannes Kepler Univ., Austria (1988).

    Google Scholar 

  87. Kutzler, B.: Careful algebraic translations of geometry theorems. In: Proc. ISSAC '89 (Portland, July 17–19, 1989), pp. 254–263.

    Google Scholar 

  88. Kutzler, B., Stifter, S.: Automated geometry theorem proving using Buchberger's algorithm. In: Proc. SYMSAC '86 (Waterloo, July 21–23, 1986), pp. 209–214.

    Google Scholar 

  89. Kutzler, B., Stifter, S.: On the application of Buchberger's algorithm to automated geometry theorem proving. JSC 2: 389–397 (1986).

    Google Scholar 

  90. Kutzler, B., Stifter, S.: A geometry theorem prover based on Buchberger's algorithm. In: LNCS 230, pp. 693–694 (1986).

    Google Scholar 

  91. Kutzler, B., Stifter, S.: Collection of computerized proofs of geometry theorems. Tech. Rep. 86-12, RISC-LINZ, Johannes Kepler Univ., Austria (1986).

    Google Scholar 

  92. Laborde, J.-M. (ed.): Intelligent learning environments — The case of geometry. Springer, Berlin-New York (1996).

    Google Scholar 

  93. Li, H.: Clifford algebra and area method. In [99]: 37–69 (1996).

    Google Scholar 

  94. Li, H., Cheng, M.: Proving theorems in elementary geometry with Clifford algebraic method. Preprint, MMRC, Academia Sinica, China (1995).

    Google Scholar 

  95. Li, Z.: Automatic implicitization of parametric objects. In [99]: 54–62 (1989).

    Google Scholar 

  96. Li, Z.: Mechanical theorem proving in the local theory of surfaces. In [66]: 25–46 (1995).

    Google Scholar 

  97. Lin, D., Liu, Z.: Some results on theorem proving in geometry over finite fields. In: Proc. ISSAC '93 (Kiev, July 6–8, 1993), pp. 292–300.

    Google Scholar 

  98. McPhee, N. F., Chou, S.-C., Gao, X.-S.: Mechanically proving geometry theorems using a combination of Wu's method and Collins' method. In: LNCS 814, pp. 401–415 (1994).

    Google Scholar 

  99. MMRC (ed.): Mathematics-Mechanization Research Preprints, nos. 1–14. Academia Sinica, China (1987–1996).

    Google Scholar 

  100. Mundy, J. L.: Reasoning about 3-D space with algebraic deduction. In: Robotics research: The third international symposium, The MIT Press, Cambridge-London, pp. 117–124 (1986).

    Google Scholar 

  101. Nevins, A. J.: Plane geometry theorem proving using forward chaining. Artif. Intell. 6: 1–23 (1975).

    Google Scholar 

  102. Pfalzgraf, J.: A category of geometric spaces: Some computational aspects. In [66]: 173–193 (1995).

    Google Scholar 

  103. Pfalzgraf, J., Stokkermans, K., Wang, D.: The robotics benchmark. In: Proc. 12-Month MEDLAR Workshop (Weinberg Castle, November 4–7, 1990), DOC, Imperial College, Univ. of London, England.

    Google Scholar 

  104. Quaife, A.: Automated development of Tarski's geometry. JAR 5: 97–118 (1989).

    Google Scholar 

  105. Rege, A.: A complete and practical algorithm for geometric theorem proving. In: Proc. 11th Ann. Symp. Comput. Geom. (Vancouver, June 5–7, 1995), pp. 277–286.

    Google Scholar 

  106. Richter-Gebert, J.: Mechanical theorem proving in projective geometry. In [66]: 139–172 (1995).

    Google Scholar 

  107. Ritt, J. F.: Differential algebra. Amer. Math. Soc., New York (1950).

    Google Scholar 

  108. Shi, H.: On the resultant formula for mechanical theorem proving. In [99]: 77–86 (1989).

    Google Scholar 

  109. Smietanski, F.: Systèmes de réécriture sur des idèaux de polynômes, géométrie et calcul formel. RAPPORT de DEA, E.N.S., Université de Jussieu Paris 7, France (1986/87).

    Google Scholar 

  110. Starkey, J. D.: EUCLID: A program which conjectures, proves and evaluates theorems in elementary geometry. Order no. 75-2780, Univ. Microfilms (1975).

    Google Scholar 

  111. Stifter, S.: Geometry theorem proving in vector spaces by means of Gröbner bases. In: Proc. ISSAC '93 (Kiev, July 6–8, 1993), pp. 301–310.

    Google Scholar 

  112. Swain, M. J., Mundy, J. L.: Experiments in using a theorem prover to prove and develop geometrical theorems in computer vision. In: Proc. IEEE Int. Conf. Robotics Automat. (San Francisco, April 7–10, 1986), pp. 280–285.

    Google Scholar 

  113. Tarski, A.: A decision method for elementary algebra and geometry. The RAND Corporation, Santa Monica (1948).

    Google Scholar 

  114. Ueberberg, J.: Interactive theorem proving and computer algebra. In: LNCS 958, pp. 1–9 (1995).

    Google Scholar 

  115. Ullmen, S.: A model-driven geometry theorem prover. AI Lab Memo no. 321, MIT, Cambridge, USA (1975).

    Google Scholar 

  116. Wang, D.-K.: Mechanical solution of a group of space geometry problems. In: Proc. IWMM '92 (Beijing, July 16–18, 1992), pp. 236–243.

    Google Scholar 

  117. Wang, D.: Mechanical approach for polynomial set and its related fields. Ph.D thesis, Academia Sinica, China (1987) [in Chinese].

    Google Scholar 

  118. Wang, D.: Proving-by-examples method and inclusion of varieties. Kexue Tongbao 33: 1121–1123 (1988).

    Google Scholar 

  119. Wang, D.: A new theorem discovered by computer prover. J. Geom. 36: 173–182 (1989).

    Google Scholar 

  120. Wang, D.: On Wu's method for proving constructive geometric theorems. In: Proc. IJCAI '89 (Detroit, August 20–25, 1989), pp. 419–424.

    Google Scholar 

  121. Wang, D.: Reasoning about geometric problems using algebraic methods. In: Medlar 24-month deliverables, DOC, Imperial College, Univ. of London, England (1991).

    Google Scholar 

  122. Wang, D.: Irreducible decomposition of algebraic varieties via characteristic sets and Gröbner bases. Comput. Aided Geom. Design 9: 471–484 (1992).

    Google Scholar 

  123. Wang, D.: Geometry theorem proving with existing technology. In: Medlar II Report PPR1, DOC, Imperial College, Univ. of London, England (1993). Also in: Proc. 1st Asian Tech. Conf. Math. (Singapore, December 18–21, 1995), 561–570.

    Google Scholar 

  124. Wang, D.: Algebraic factoring and geometry theorem proving. In: LNCS 814, pp. 386–400 (1994).

    Google Scholar 

  125. Wang, D.: Reasoning about geometric problems using an elimination method. In: Automated practical reasoning: Algebraic approaches (Pfalzgraf, J., Wang, D., eds.), Springer, Wien-New York, pp. 147–185 (1995).

    Google Scholar 

  126. Wang, D.: Elimination procedures for mechanical theorem proving in geometry. In [66]: 1–24 (1995).

    Google Scholar 

  127. Wang, D.: A method for proving theorems in differential geometry and mechanics. J. Univ. Comput. Sci. 1: 658–673 (1995).

    Google Scholar 

  128. Wang, D.: GEOTHER: A geometry theorem prover. In: Proc. CADE-13 (New Brunswick, July 30–August 3, 1996), to appear.

    Google Scholar 

  129. Wang, D., Gao, X.-S.: Geometry theorems proved mechanically using Wu's method — Part on Euclidean geometry. In [99]: 75–106 (1987).

    Google Scholar 

  130. Wang, D., Hu, S.: A mechanical proving system for constructible theorems in elementary geometry. J. SSMS 7: 163–172 (1987) [in Chinese].

    Google Scholar 

  131. Winkler, F.: A geometrical decision algorithm based on the Gröbner bases algorithm. In: LNCS 358, pp. 356–363 (1988).

    Google Scholar 

  132. Winkler, F.: Gröbner bases in geometry theorem proving and simplest degeneracy conditions. Math. Pannonica 1: 15–32 (1990).

    Google Scholar 

  133. Winkler, F.: Automated theorem proving in nonlinear geometry. In: Issues in robotics and nonlinear geometry (Hoffmann, C., ed.), JAI Press, Greenwich, pp. 183–197 (1992).

    Google Scholar 

  134. Wong, R.: Construction heuristics for geometry and a vector algebra representation of geometry. Tech. Memo. 28, Project MAC, MIT, Cambridge, USA (1972).

    Google Scholar 

  135. Wu, T.-J.: On a collision problem. In [99]: 96–104 (1991).

    Google Scholar 

  136. Wu, W.-t.: On the decision problem and the mechanization of theorem-proving in elementary geometry. Sci. Sinica 21: 159–172 (1978). Also in [9], pp. 213–234 (1984).

    Google Scholar 

  137. Wu, W.-t.: On the mechanization of theorem-proving in elementary differential geometry. Sci. Sinica Special Issue on Math. (I): 94–102 (1979) [in Chinese].

    Google Scholar 

  138. Wu, W.-t.: Mechanical theorem proving in elementary geometry and elementary differential geometry. In: Proc. 1980 Beijing Symp. Diff. Geom. Diff. Eqs. (Beijing, August 18–September 21, 1980), pp. 1073–1092.

    Google Scholar 

  139. Wu, W.-t.: Toward mechanization of geometry — Some comments on Hilbert's “Grundlagen der Geometrie”. Acta Math. Scientia 2: 125–138 (1982).

    Google Scholar 

  140. Wu, W.-t.: Some remarks on mechanical theorem-proving in elementary geometry. Acta Math. Scientia 3: 357–360 (1983).

    Google Scholar 

  141. Wu, W.-t.: Basic principles of mechanical theorem proving in elementary geometries. J. SSMS 4: 207–235 (1984). Also in JAR 2: 221–252 (1986).

    Google Scholar 

  142. Wu, W.-t.: Basic principles of mechanical theorem proving in geometries (part on elementary geometries). Science Press, Beijing (1984) [in Chinese]. English Translation, Springer, Wien-New York (1994).

    Google Scholar 

  143. Wu, W.-t.: Some recent advances in mechanical theorem-proving of geometries. In [9], pp. 235–241 (1984).

    Google Scholar 

  144. Wu, W.-t.: A mechanization method of geometry I. Chinese Quart. J. Math. 1: 1–14 (1986).

    Google Scholar 

  145. Wu, W.-t.: A mechanization method of geometry and its applications I. J. SSMS 6: 204–216 (1986).

    Google Scholar 

  146. Wu, W.-t.: A report on mechanical theorem proving and mechanical theorem discovering in geometries. Adv. Sci. China Math. 1: 175–198 (1986).

    Google Scholar 

  147. Wu, W.-t.: A constructive theory of differential algebraic geometry. In: Lecture Notes in Math. 1255, pp. 173–189 (1987).

    Google Scholar 

  148. Wu, W.-t.: A mechanization method of geometry and its applications II. Kexue Tongbao 32: 585–588 (1987).

    Google Scholar 

  149. Wu, W.-t.: On reducibility problem in mechanical theorem proving of elementary geometries. Chinese Quart. J. Math. 2: 1–20 (1987).

    Google Scholar 

  150. Wu, W.-t.: A mechanization method of geometry and its applications III. SSMS 1: 1–17 (1988).

    Google Scholar 

  151. Wu, W.-t.: A mechanization method of geometry and its applications IV. SSMS 2: 97–109 (1989).

    Google Scholar 

  152. Wu, W.-t.: Equations-solving and theorems-proving — Zero-set formulation and ideal formulation. In: Proc. Asian Math. Conf. (Hong Kong, August 14–18, 1990), pp. 1–10.

    Google Scholar 

  153. Wu, W.-t.: Mechanical theorem proving of differential geometries and some of its applications in mechanics. JAR 7: 171–191 (1991).

    Google Scholar 

  154. Wu, W.-t.: A report on mechanical geometry theorem proving. Progr. Natur. Sci. 2: 1–17 (1992).

    Google Scholar 

  155. Wu, W.-t.: A mechanization method of equations solving and theorem proving. In: Issues in robotics and nonlinear geometry (Hoffmann, C., ed.), JAI Press, Greenwich, pp. 103–138 (1992).

    Google Scholar 

  156. Wu, W.-t.: On problems involving inequalities. In [99]: 1–13 (1992).

    Google Scholar 

  157. Wu, W.-t.: On a finiteness theorem about problems involving inequalities. SSMS 7: 193–200 (1994).

    Google Scholar 

  158. Wu, W.-t.: Central configurations in planet motions and vortex motions. In [99]: 1–14 (1995).

    Google Scholar 

  159. Wu, W.-t., Lü, X.-L.: Triangles with equal bisectors. People's Edu. Press, Beijing (1985) [in Chinese].

    Google Scholar 

  160. Wu, W.-t., Wang, D.-K.: The algebraic surface fitting problem in CAGD. Math. Practice Theory no. 3: 26–31 (1994) [in Chinese].

    Google Scholar 

  161. Xu, C., Shi, Q., Cheng, M.: A global stereo vision method based on Wu-solver. In: Proc. GMICV '95 (Xi'an, April 27–29, 1995), pp. 198–205.

    Google Scholar 

  162. Xu, L., Chen, J.: AUTOBASE: A system which automatically establishes the geometry knowledge base. In: Proc. COMPINT: Computer aided technologies (Montreal, September 8–12, 1985), pp. 708–714.

    Google Scholar 

  163. Xu, L., Chen, J., Yang, L.: Solving plane geometry problem by learning. In: Proc. IEEE 1st Int. Conf. Comput. Appl. (Beijing, June 20–22, 1984), pp. 862–869.

    Google Scholar 

  164. Yang, L.: A new method of automated theorem proving. In: The mathematical revolution inspired by computing (Johnson, J., Loomes, M., eds.), Oxford Univ. Press, New York, pp. 115–126 (1991).

    Google Scholar 

  165. Yang, L., Zhang, J.-Z.: Searching dependency between algebraic equations: An algorithm applied to automated reasoning. In: Artificial intelligence in mathematics (Johnson, J., McKee, S., Vella, A., eds.), Oxford Univ. Press, Oxford, pp. 147–156 (1994).

    Google Scholar 

  166. Yang, L., Zhang, J.-Z., Hou, X.-R.: A criterion for dependency of algebraic equations, with applications to automated theorem proving. Sci. China Ser. A 37: 547–554 (1994).

    Google Scholar 

  167. Yang, L., Zhang, J.-Z., Hou, X.-R.: An efficient decomposition algorithm for geometry theorem proving without factorization. In: Proc. ASCM '95 (Beijing, August 18–20, 1995), pp. 33–41.

    Google Scholar 

  168. Yang, L., Zhang, J.-Z., Li, C.-Z.: A prover for parallel numerical verification of a class of constructive geometry theorems. In: Proc. IWMM '92 (Beijing, July 16–18, 1992), pp. 244–250.

    Google Scholar 

  169. Zhang, J.-Z.: How to solve geometry problems using areas. Shanghai Edu. Publ., Shanghai (1982) [in Chinese].

    Google Scholar 

  170. Zhang, J.-Z., Chou, S.-C., Gao, X.-S.: Automated production of traditional proofs for theorems in Euclidean geometry I. In [66]: 109–137 (1995).

    Google Scholar 

  171. Zhang, J.-Z., Yang, L., Deng, M.-K.: The parallel numerical method of mechanical theorem proving. Theoret. Comput. Sci. 74: 253–271 (1990).

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Laboratoire LEIBNIZ, Institut IMAG, 46, avenue Félix Viallet, 38031, Grenoble Cedex, France

    Dongming Wang

Authors
  1. Dongming Wang
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Jacques Calmet John A. Campbell Jochen Pfalzgraf

Rights and permissions

Reprints and permissions

Copyright information

© 1996 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Wang, D. (1996). Geometry machines: From AI to SMC. In: Calmet, J., Campbell, J.A., Pfalzgraf, J. (eds) Artificial Intelligence and Symbolic Mathematical Computation. AISMC 1996. Lecture Notes in Computer Science, vol 1138. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61732-9_60

Download citation

  • DOI: https://doi.org/10.1007/3-540-61732-9_60

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-61732-7

  • Online ISBN: 978-3-540-70740-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation