Books and Special Issues

*

Arnon, D. S., Buchberger, B. (eds.): Algorithms in real algebraic geometry. Special Issue of J. Symb. Comput. 5(1-2), Academic Press, London (1988).

*

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

*

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

*

Bokowski, J., Sturmfels, B.: Computational synthetic geometry. LNM 1355, Springer, Berlin Heidelberg (1989).

*

Chen, F., Wang, D. (eds.): Geometric computation. World Scientific, Singapore (2004).

*

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

*

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

*

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

*

Du, D.-Z., Hwang, F. (eds.): Computing in Euclidean geometry. World Scientific, Singapore (1992). 2nd edition (1995).

*

Gao, X.-S., Wang, D., Yang, L. (eds.): Automated deduction in geometry - ADG '98 proceedings. LNAI 1669, Springer, Berlin Heidelberg (1999).

*

Hoffmann, C. M.: Geometric and solid modeling: An introduction. Morgan Kaufmann, San Mateo (1989).

*

Hoffmann, C. M. (ed.): Issues in robotics and nonlinear geometry. JAI Press, Greenwich (1992).

*

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).

*

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

*

Kramer, G.: Solving geometric constraint systems. The MIT Press, Cambridge (1992).

*

Kueker, D., Smith, C. (eds.): Learning and geometry: Computational approaches. Birkhäuser, Boston (1996).

*

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

*

McCune, W., Padmanabhan, R.: Automated deduction in equational logic and cubic curves. Springer, Berlin Heidelberg (1996).

*

MMRC (ed.): Mathematics mechanization research preprints (1-15). Academia Sinica, China (1987-1997).

*

Richter-Gebert, J., Kortenkamp, U. H.: The interactive geometry software Cinderella. Springer, Berlin Heidelberg (1999).

*

Richter-Gebert, J., Kortenkamp, U. H.: User manual for the interactive geometry software Cinderella. Springer, Berlin Heidelberg (2000).

*

Richter-Gebert, J., Kortenkamp, U. H.: Cinderella: Die interaktive Geometrie-Software. Springer, Berlin Heidelberg (2001).

*

Richter-Gebert, J., Kortenkamp, U. H.: Benutzerhandbuch für die interaktive Geometrie-Software Cinderella. Springer, Berlin Heidelberg (2001).

*

Richter-Gebert, J., Kortenkamp, U. H.: Cinderella: Software interattivo di geometria. Springer, Berlin Heidelberg (2001).

*

Richter-Gebert, J., Wang, D. (eds.): Proceedings of ADG 2000 - The third international workshop on automated deduction in geometry (Zurich, Switzerland, September 25-27, 2000). 290 pages, available from Theoretische Informatik, ETH Zentrum, Zurich, Switzerland.

*

Richter-Gebert, J., Wang, D. (eds.): Automated deduction in geometry - ADG 2000 revised papers. LNAI 2061, Springer, Berlin Heidelberg (2001).

*

Sturmfels, B., White, N. L. (eds.): Invariant-theoretic algorithms in geometry. Special issue of J. Symb. Comput. 11(5-6), Academic Press, London (1991).

*

Tarski, A.: A decision method for elementary algebra and geometry. The RAND Corporation, Santa Monica (1948). 2nd edition, Univ. of California Press, Berkeley Los Angeles (1951).

*

Wang, D. (ed. in cooperation with R. Caferra, L. Fariñas del Cerro and H. Shi): Automated deduction in geometry. LNAI 1360, Springer, Berlin Heidelberg (1997).

*

Wang, D.: Elimination methods. Springer, Wien New York (2001).

*

Wang, D.: Elimination practice: Software tools and applications. Imperial College Press, London (2004).

*

Woodwark, J. (ed.): Geometric reasoning. Oxford Univ. Press, Oxford (1990).

*

Wu, W.-t.: Basic principles of mechanical theorem proving in geometries - Part on elementary geometries. Science Press, Beijing (1984) [in Chinese].

*

Wu, W.-t. Mechanical theorem proving in geometries: Basic principles (translated from the Chinese by X. Jin and D. Wang). Springer, Wien New York (1994).

*

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

*

Yang, L., Zhang, J.-Z., Hou, X.-R.: Nonlinear algebraic equation system and automated theorem proving. Shanghai Sci & Tech Education Publ. House, Shanghai (1996) [in Chinese].

*

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

*

Zhang, J.-Z.: A new approach to plane geometry. Sichuan Education Publ. Inc., Chengdu (1992) [in Chinese].

*

Zhang, J.-Z., Cao, P.-S.: From education of mathematics to mathematics for education. Sichuan Education Publ. Inc., Chengdu (1988) [in Chinese].

Articles

*

Alberti, M. A., Carrà Ferro, G., Lammoglia, B., Torelli, M.: The dimension method in elementary and differential geometry. Ann. Math. Artif. Intell. 13: 47-71 (1995).

*

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.

*

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

*

Arbab, F., Wang, B.: Reasoning about geometric constraints. In: Intelligent CAD II (Yoshikawa, H., Holden, T., eds.), Elsevier, North-Holland, pp. 93-107 (1990).

*

Arnon, D. S.: Algorithms for the geometry of semi-algebraic sets. Ph.D thesis, Comput. Sci. Dept., Univ. of Wisconsin-Madison, USA (1981).

*

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

*

Arnon, D. S., Mignotte, M.: On mechanical quantifier elimination for elementary algebra and geometry. J. Symb. Comput. 5: 237-259 (1988).

*

Aubry, P., Wang, D.: Reasoning about surfaces using differential zero and ideal decomposition. In: Springer's LNAI 2061, pp. 154-174 (2001).

*

Balbiani, P.: Equation solving in projective planes and planar ternary rings. In: Springer's LNCS 850, pp. 95-113 (1994).

*

Balbiani, P.: Equation solving in geometrical theories. In: Springer's LNCS 968, pp. 31-55 (1995).

*

Balbiani, P., Dugat, V., Lopez, A.: Le raisonnement sur les figures de la géométrie projective. Rapport Irit/94-5-R, IRIT, Univ. Paul Sabatier, France (1994).

*

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

*

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.

*

Barry, M., Cyrluk, D., Kapur, D, Mundy, J.: Multi-level geometric reasoning system for vision. In: Proc. Int. Workshop Geom. Reason. (Oxford, June 30 - July 3, 1986).

*

Bazzotti, L., Dalzotto, G., Robbiano, L.: Remarks on geometric theorem proving. In: Springer's LNAI 2061, pp. 104-128 (2001).

*

Beutelspacher, A., Ueberberg, J.: Symbolic incidence geometry: Proposal for doing geometry with a computer. ACM SIGSAM 27(2): 19-29; 27(3): 9-24 (1992).

*

Bokowski, J.: Effective methods in computational synthetic geometry. In: Springer's LNAI 2061, pp. 175-192 (2001).

*

Bondyfalat, D., Mourrain, B., Papadopoulo, T.: An application of automatic theorem proving in computer vision. In: Springer's LNAI 1669, pp. 207-231 (1999).

*

Botana, F.: A web-based intelligent system for geometric discovery. In: Springer's LNCS 2657, pp. 801-810 (2003).

*

Botana, F., Valcarce, J. L.: A software tool for the investigation of plane loci. Math. Comput. Simulation 61(2): 139-152 (2003).

*

Bouhineau, D.: Solving geometrical constraint systems using CLP based on linear constraint solver. In: Springer's LNCS 1138, pp. 274-288 (1996).

*

Boy de la Tour, T., Fèvre, S., Wang, D.: Clifford term rewriting for geometric reasoning in 3D. In: Springer's LNAI 1669, pp. 130-155 (1999).

*

Brüderlin, B.: Using Prolog for constructing geometric objects defined by constraints. In: Springer's LNCS 204, p. 448 (1985).

*

Brüderlin, B.: Automatizing geometric proofs and constructions. In: Springer's LNCS 333, pp. 232-252 (1988).

*

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).

*

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

*

Bulmer, M., Fearnley-Sander, D., Stokes, T.: The kinds of truth of geometry theorems. In: Springer's LNAI 2061, pp. 129-142 (2001).

*

Caferra, R., Peltier, N., Puitg, F.: Emphasizing human techniques in automated geometry theorem proving: A practical realization. In: Springer's LNAI 2061, pp. 269-306 (2001).

*

Carrà Ferro, G.: An extension of a procedure to prove statements in differential geometry. J. Automat. Reason. 12: 351-358 (1994).

*

Carrà Ferro, G., Gallo, G.: A procedure to prove geometrical statements. In: Springer's LNCS 356, pp. 141-150 (1987).

*

Carrà Ferro, G., Gallo, G.: A procedure to prove statements in differential geometry. J. Automat. Reason. 6: 203-209 (1990).

*

Carrà Ferro, G., Gallo, G., Gennaro, R.: Probabilistic verification of elementary geometry statements. In: Springer's LNAI 1360, pp. 87-101 (1997).

*

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

*

Chou, S.-C.: Proving elementary geometry theorems using Wu's algorithm. In: Automated theorem proving: After 25 years (Bledsoe, W. W., Loveland, D. W., eds.), AMS, Providence, pp. 243-286 (1984).

*

Chou, S.-C.: Proving and discovering theorems in elementary geometries using Wu's method. Ph.D thesis, Univ. of Texas at Austin, USA (1985).

*

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

*

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

*

Chou, S.-C.: An introduction to Wu's method for mechanical theorem proving in geometry. J. Automat. Reason. 4: 237-267 (1988).

*

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.

*

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

*

Chou, S.-C., Gao, X.-S.: A collection of 120 computer solved geometry problems in mechanical formula derivation. Tech. Rep. TR-89-22, Dept. of Comput. Sci., Univ. of Texas at Austin, USA (1989).

*

Chou, S.-C., Gao, X.-S.: Methods for mechanical geometry formula deriving. In: Proc. ISSAC '90 (Tokyo, August 20-24, 1990), pp. 265-270.

*

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

*

Chou, S.-C., Gao, X.-S.: Theorems proved automatically using Wu's method - Part on differential geometry (space curves) and mechanics. Math. Mech. Res. Preprints 6: 37-55 (1991).

*

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

*

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).

*

Chou, S.-C., Gao, X.-S.: Mechanical theorem proving in Riemann geometry using Wu's method. In: Computer mathematics (Tianjin, 1991), Nankai Ser. Pure Appl. Math. Theoret. Phys. 5, World Scientific, River Edge, pp. 136-157 (1993).

*

Chou, S.-C., Gao, X.-S.: Automated reasoning in differential geometry and mechanics using the characteristic set method I & II. J. Automat. Reason. 10: 161-189 (1993).

*

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

*

Chou, S.-C., Gao, X.-S.: The computer searches for Pascal conics. Comput. Math. Appl. 29: 63-71 (1995).

*

Chou, S.-C., Gao, X.-S.: A survey of geometric reasoning using algebraic methods. In: Learning and geometry: Computational approaches (Kueker, D. W., Smith, C., eds.), Birkhäuser, Boston, pp. 97-119 (1996).

*

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. M., ed.), JAI Press, Greenwich, pp. 139-181 (1992).

*

Chou, S.-C., Gao, X.-S., Liu, Z., Wang, D.-K., Wang, D.: Geometric theorem provers and algebraic equation solvers. In: Mathematics mechanization and applications (Gao, X.-S., Wang, D., eds.), Academic Press, London, pp. 491-505 (2000).

*

Chou, S.-C., Gao, X.-S., Yang, L., Zhang, J.-Z.: A collection of 90 automatically proved geometry theorems in non-Euclidean geometries. Tech. Rep. TR-WSU-94-10, Wichita State Univ., USA (1994).

*

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.

*

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.

*

Chou, S.-C., Gao, X.-S., Zhang, J.-Z.: The area method and affine geometries over any fields. Math. Mech. Res. Preprints 10: 92-100 (1993).

*

Chou, S.-C., Gao, X.-S., Zhang, J.-Z.: A rule based geometry theorem prover using full angles. Math. Mech. Res. Preprints 11: 72-103 (1994).

*

Chou, S.-C., Gao, X.-S., Zhang, J.-Z.: Vectors and automated geometry reasoning. Math. Mech. Res. Preprints 11: 104-127 (1994).

*

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

*

Chou, S.-C., Gao, X.-S., Zhang, J.-Z.: Automated geometry theorem proving and geometry education. In: Proc. 1st Asian Tech. Conf. Math. (Singapore, December 18-21, 1995), pp. 319-328.

*

Chou, S.-C., Gao, X.-S., Zhang, J.-Z.: A fixpoint approach to automated geometry theorem proving. Tech. Rep. WSUCS-95-2, Wichita State Univ., USA (1995).

*

Chou, S.-C., Gao, X.-S., Zhang, J.-Z.: Automated generation of readable proofs with geometric invariants I & II. J. Automat. Reason. 17: 325-370 (1996).

*

Chou, S.-C., Gao, X.-S., Zhang, J.-Z.: An introduction to geometry expert. In: Springer's LNAI 1104, pp. 235-239 (1996).

*

Chou, S.-C., Gao, X.-S., Zhang, J.-Z.: Recent advances of automated geometry theorem proving with high level geometry invariants. In: Proc. ASCM '96 (Kobe, 1996), pp. 173-186.

*

Chou, S.-C., Gao, X.-S., Zhang, J.-Z.: Automated solution of two-dimensional geometric constraint problems. In: Proc. ASCM '96 (Kobe, 1996), pp. 153-164.

*

Chou, S.-C., Gao, X.-S., Zhang, J.-Z.: Automated generation of construction steps for geometric constraint problems. In: Automated reasoning and its applications (Veroff, R., ed.), The MIT Press, Cambridge, pp. 49-69 (1997).

*

Chou, S.-C., Gao, X.-S., Zhang, J.-Z.: A deductive database approach to automated geometry theorem proving and discovering. J. Automat. Reason. 25: 219-246 (1996).

*

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.

*

Chou, S.-C., Lin, D.: Wu's method for automated geometry theorem proving and discovering. In: Mathematics mechanization and applications (Gao, X.-S., Wang, D., eds.), Academic Press, London, pp. 125-146 (2000).

*

Chou, S.-C., Rathi, M.: Machine proofs of geometry theorems. In: Computing in Euclidean geometry (Du, D.-Z., Hwang, F. K., eds.), World Scientific, Singapore, pp. 91-115 (1992).

*

Chou, S.-C., Schelter, W. F.: Proving geometry theorems with rewrite rules. J. Automat. Reason. 2: 253-273 (1986).

*

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).

*

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).

*

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

*

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).

*

Coelho, H., Pereira, L. M.: Automated reasoning in geometry theorem proving with Prolog. J. Automat. Reason. 2: 329-390 (1986).

*

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

*

Connolly, C. I., Kapur, D., Mundy, J. L., Weiss, R.: GEometer: A system for modeling and algebraic manipulation. In: Proc. DARPA Workshop Image Understanding (Palo Alto, May 1989), pp. 797-804.

*

Conti, P., Traverso, C.: A case of automatic theorem proving in Euclidean geometry: The Maclane 8_3 theorem. In: Springer's LNCS 948, pp. 183-193 (1995).

*

Conti, P., Traverso, C.: Algebraic and semialgebraic proofs: Methods and paradoxes. In: Springer's LNAI 2061, pp. 83-103 (2001).

*

Cox, D., Little, J., O'Shea, D.: Robotics and automated geometric theorem proving. Chapter 6 in: Ideals, varieties and algorithms, Springer, New York Berlin (1992). 2nd edition (1997).

*

Crapo, H., Richter-Gebert, J.: Automatic proving of geometric theorems. In: Invariant methods in discrete and computational geometry (White, N. L., ed.). Kluwer, Dordrecht, pp. 167-196 (1995).

*

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

*

de Alwis, T.: Normal lines drawn to a parabola and geometric constructions. In: Proc. ATCM98 (Tsukuba, August 24-28, 1998), pp. 389-398.

*

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.

*

Dehlinger, C., Dufourd, J.-F., Schreck, P.: Higher-order intuitionistic formalization and proofs in Hilbert's elementary geometry. In: Springer's LNAI 2061, pp. 307-324 (2001).

*

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

*

Dolzmann, A.: Solving geometric problems with real quantifier elimination. In: Springer's LNAI 1669, pp. 14-29 (1999).

*

Dolzmann, A., Sturm, T., Weispfenning, V.: A new approach for automatic theorem proving in real geometry. J. Automat. Reason. 21: 357-380 (1998).

*

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

*

Evans, T. G.: A heuristic program to solve geometry analogy problems. In: Semantic information processing (Minsky, M. L., ed.), The MIT Press, Cambridge (1969).

*

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).

*

Fearnley-Sander, D.: Using and computing symmetry in geometry proofs. In: Proc. Conf. AI Simul. Behav. (Ross, P., ed.).

*

Fearnley-Sander, D.: Plane Euclidean reasoning. In: Springer's LNAI 1669, pp. 86-110 (1999).

*

Fearnley-Sander, D., Stokes, T.: Area in Grassmann geometry. In: Springer's LNAI 1360, pp. 141-170 (1997).

*

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

*

Fèvre, S.: Integration of reasoning and algebraic calculus in geometry. In: Springer's LNAI 1360, pp. 218-234 (1997).

*

Fèvre, S., Peltier, N.: Two problems in geometry solved by using automated model builders. AAR Newsletter 38 (1997).

*

Fèvre, S., Wang, D.: Proving geometric theorems using Clifford algebra and rewrite rules. In: Springer's LNAI 1421, pp. 17-32 (1998).

*

Fèvre, S., Wang, D.: Combining algebraic computing and term-rewriting for geometry theorem proving. In: Springer's LNAI 1476, pp. 145-156 (1998).

*

Fèvre, S., Wang, D.: Combining Clifford algebraic computing and term-rewriting for geometric theorem proving. Fundamenta Informaticae 39 (1-2): 85-104 (1999).

*

Fleuriot, J. D.: Nonstandard geometric proofs. In: Springer's LNAI 2061, pp. 246-268 (2001).

*

Fleuriot, J. D., Paulson, L. C.: A combination of nonstardard analysis and geometry theorem proving, with application to Newton's principia. In: Springer's LNAI 1421, pp. 3-16 (1998).

*

Fleuriot, J. D., Paulson, L. C.: Proving Newton's Propositio Kepleriana using geometry and nonstandard analysis in Isabelle. In: Springer's LNAI 1669, pp. 47-66 (1999).

*

Gao, X.-S.: Trigonometric identities and mechanical theorem proving in elementary geometry. J. Syst. Sci. Math. Sci. 7: 264-272 (1987) [in Chinese].

*

Gao, X.-S.: Constructive methods for polynomial sets and their applications. Ph.D thesis, Academia Sinica, China (1988) [in Chinese].

*

Gao, X.-S.: Transcendental functions and mechanical theorem proving in elementary geometries. J. Automat. Reason. 6: 403-417 (1990).

*

Gao, X.-S.: Transformation theorems among Cayley-Klein geometries. Syst. Sci. Math. Sci. 5: 263-273 (1992).

*

Gao, X.-S.: An introduction to Wu's method of mechanical geometry theorem proving. In: Automated reasoning (Shi, Z., ed.), Elsevier, North-Holland, pp. 13-21 (1992).

*

Gao, X.-S.: Automated geometry diagram construction and engineering geometry. In: Springer's LNAI 1669, pp. 232-257 (1999).

*

Gao, X.-S.: Building dynamic mathematical models with Geometry Expert - III. A geometry deductive batabase. In: Proc. ATCM '99 (Guangzhou, December 17-21, 1999), pp. 153-162.

*

Gao, X.-S.: Search methods revisited. In: Mathematics mechanization and applications (Gao, X.-S., Wang, D., eds.), Academic Press, London, pp. 253-271 (2000).

*

Gao, X.-S., Chou, S.-C.: Solving geometric constraint systems I & II. J. CAD (to appear).

*

Gao, X.-S., Huang, L.-D., Jiang, K.: A hybrid method for solving geometric constraint problems. In: Springer's LNAI 2061, pp. 16-25 (2001).

*

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.

*

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

*

Gao, X.-S., Zhu, C., Huang, Y.: Building dynamic mathematical models with Geometry Expert - I. Geometric transformations, funtions and plane curves. In: Proc. ATCM98 (Tsukuba, August 24-28, 1998), pp. 216-224.

*

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

*

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.

*

Gehrke, W., Pfalzgraf, J.: Computer-aided construction of finite geometric spaces: Automated verification of geometric constraints. J. Automat. Reason. 26: 139-160 (2001).

*

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

*

Goguen, J. A.: Modular algebraic specification of some basic geometrical constructions. Artif. Intell. 37: 121-156 (1988).

*

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

*

Grünbaum, B., Shephard, G. C.: From Menelaus to computer assisted proofs in geometry. Preprint, Washington State Univ., USA (1993).

*

Guergueb, A.: Exemples de démonstration automatique en géométrie réelle. Ph.D thesis, Univ. de Rennes I, France (1994).

*

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.

*

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.

*

Havel, T. F.: Some examples of the use of distances as coordinates for Euclidean geometry. J. Symb. Comput. 11: 579-593 (1991).

*

Havel, T. F.: Computational synthetic geometry with Clifford algebra. In: Springer's LNAI 1360, pp. 102-114 (1997).

*

Havel, T. F.: Qubit logic, algebra and geometry. In: Springer's LNAI 2061, pp. 228-245 (2001).

*

Hillgarter, E., Winkler, F.: Points on algebraic curves and the parametrization problem. In: Springer's LNAI 1360, pp. 189-207 (1997).

*

Hoffmann, C. M., Vermeer, P. J.: Geometric constraint solving in R^2 and R^3. In: Computing in Euclidean geometry (Du, D.-Z., Hwang, F. K., eds.), 2nd edition, World Scientific, Singapore, pp. 266-298 (1995).

*

Hoffmann, C. M., Yuan, B.: On spatial constraint solving approaches. In: Springer's LNAI 2061, pp. 1-15 (2001).

*

Hong, H., Wang, D., Winkler, F.: Short description of existing provers. Ann. Math. Artif. Intell. 13: 195-202 (1995).

*

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

*

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

*

Hou, X.: Proving by examples. In: Mathematics mechanization and applications (Gao, X.-S., Wang, D., eds.), Academic Press, London, pp. 231-251 (2000).

*

Hou, X., Li, H., Wang, D., Yang, L.: "Russian Killer" No. 2: A challenging geometric theorem with human and machine proofs. Math. Intell. 23: 9-15 (2001).

*

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

*

Iba, H., Inoue, H.: Geometric reasoning based on algebraic method I & II. J. Artif. Intell. l5(3): 46-69 (199?).

*

Kalkbrener, M.: A generalized Euclidean algorithm for geometry theorem proving. Ann. Math. Artif. Intell. 13: 73-95 (1995).

*

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

*

Kapur, D.: Using Gröbner bases to reason about geometry problems. J. Symb. Comput. 2: 399-408 (1986).

*

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

*

Kapur, D.: Automated geometric reasoning: Dixon resultants, Gröbner bases, and characteristic sets. In: Springer's LNAI 1360, pp. 1-36 (1997).

*

Kapur, D., Mundy, J. L.: Wu's method: An informal introduction. In: Proc. Int. Workshop Geom. Reason. (Oxford, June 30 - July 3, 1986).

*

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

*

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.

*

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.

*

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

*

Ko, H.-P.: On algebraic formulation of Wu's method and Chou's method - Methods to prove certain theorems in elementary geometry. Tech. Rep. 85CRD099, General Electric Co., Schenectady, USA (1985).

*

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

*

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).

*

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

*

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).

*

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

*

Koedinger, K. R., Anderson, J. R.: Abstract planning and perceptual chunks: Elements of expertise in geometry. Cogn. Sci. 14: 511-550 (1990).

*

Koepf, W.: Gröbner bases and triangles. Int. J. Comput. Algebra Math. Educ. 4: 371-386 (1997).

*

Kortenkamp, U., Richter-Gebert, J.: Decision complexity in dynamic geometry. In: Springer's LNAI 2061, pp. 193-198 (2001).

*

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

*

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

*

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

*

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

*

Kutzler, B., Stifter, S.: On the application of Buchberger's algorithm to automated geometry theorem proving. J. Symb. Comput. 2: 389-397 (1986).

*

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

*

Kutzler, B., Stifter, S.: New approaches to computerized proofs of geometry theorems. Tech. Rep. 86-5, RISC-Linz Johannes Kepler Univ., Austria (1986).

*

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

*

Lee, J. Y.: A 2D geometric constraint solver for parametric design using graph analysis and reduction. In: Springer's LNAI 1669, pp. 258-274 (1999).

*

Li, C.-Z., Zhang, J.-Z.: Readable machine solving in geometry and ICAI software MSG. In: Springer's LNAI 1669, pp. 67-85 (1999).

*

Li, D.: Replacing the axioms for connecting lines and intersection points by two single axioms. AAR Newsletter 37 (1997).

*

Li, D.: Is von Plato's axiomatization complete for elementary geometry? AAR Newsletter 37 (1997).

*

Li, D.: Three axioms of von Plato's axiomatization of constructive projective geometry are not independent. AAR Newsletter 37 (1997).

*

Li, H.: New explorations on mechanical theorem proving of geometries. Ph.D thesis, Beijing Univ., China (1994).

*

Li, H.: Automated reasoning with differential forms. In: Proc. ASCM '95 (Beijing, August 18-20, 1995), pp. 29-32.

*

Li, H.: Clifford algebra and area method. Math. Mech. Res. Preprints 14: 37-69 (1996).

*

Li, H.: Clifford algebra and Lobachevski geometry. In: Clifford algebras and their applications in mathematical physics (Dietrich, V. et al., eds.), D. Reidel, Dordrecht, pp. 239-245 (1996).

*

Li, H.: Ordering in mechanical geometry theorem proving. Sci. China (Ser. A) 40: 225-233 (1997).

*

Li, H.: On mechanical theorem proving in differential geometry - Local theory of surfaces. Sci. China (Ser. A) 40: 350-356 (1997).

*

Li, H.: Hyperbolic geometry with Clifford algebra. Acta Appl. Math. 48: 317-358 (1997).

*

Li, H.: Some applications of Clifford algebra to geometries. In: Springer's LNAI 1669, pp. 156-179 (1999).

*

Li, H.: Vectorial equations solving for mechanical geometry theorem proving. J. Automat. Reason. 25: 83-121 (2000).

*

Li, H.: Mechanical theorem proving in differential geometry. In: Mathematics mechanization and applications (Gao, X.-S., Wang, D., eds.), Academic Press, London, pp. 147-173 (2000).

*

Li, H.: Clifford algebra approaches to mechanical geometry theorem proving. In: Mathematics mechanization and applications (Gao, X.-S., Wang, D., eds.), Academic Press, London, pp. 205-229 (2000).

*

Li, H.: Doing geometric research with Clifford algebra. In: Clifford algebras and their applications in mathematical physics, vol. 1 (Ablamowicz, R., Fauser, B., eds.), Birkhäuser, Boston, pp. 195-217 (2000).

*

Li, H.: Automated theorem proving. In: Advances in geometric algebra with applications (Bayro-Corrochano, E., Sobczyk, G., eds.), Birkhäuser, Boston, pp. 112-122 (2001).

*

Li, H.: Clifford algebras in geometric computation. In: Geometric computation (Chen, F., Wang, D., eds.), World Scientific, Singapore, pp. 221-247 (2003).

*

Li, H., Cheng, M.: Proving theorems in elementary geometry with Clifford algebraic method. Chinese Math. Progress 26: 357-371 (1997).

*

Li, H., Cheng, M.: Ordering in mechanical theorem proving in differential geometry. Acta Math. Appl. Sinica 14(4): 358-362 (1998).

*

Li, H., Cheng, M.: Clifford algebraic reduction method for automated theorem proving in differential geometry. J. Automat. Reason. 21: 1-21 (1998).

*

Li, H., Shi, H.: On Erdos' ten-point problem. Acta Math. Sinica (New Ser.) 13: 221-230 (1997).

*

Li, H., Wu, Y.: Automated theorem proving in projective geometry with bracket algebra. In: Proc. ASCM 2000 (Chiang Mai, December 17-21, 2000), pp. 120-129.

*

Li, H., Wu, Y.: Automated theorem proving in incidence geometry - A bracket algebra based elimination method. In: Springer's LNAI 2061, pp. 199-227 (2001).

*

Li, Y.-B.: Automated derivation of unknown relations and determination of geometric loci. In: Geometric computation (Chen, F., Wang, D., eds.), World Scientific, Singapore, pp. 299-321 (2003).

*

Li, Z.: Mechanical theorem proving in the local theory of surfaces. Ann. Math. Artif. Intell. 13: 25-46 (1995).

*

Lin, D., Liu, Z.: Some results on theorem proving in finite geometry. In: Proc. IWMM '92 (Beijing, July 16-18, 1992), pp. 222-235 (1992).

*

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.

*

Lopez, A.: Démonstration automatique en géométrie par réduction de figures. Ph.D thesis, Univ. Paul Sabatier, France (1995).

*

Mainguené, J.: Méthode de Wu, courbes réelles et démonstration automatique en géométrie. Ph.D thesis, Univ. de Rennes I, France (1994).

*

Matsuyama, T., Nitta, T.: Geometric theorem-proving by integrated logical and algebraic reasoning. Artif. Intell. 75: 93-413 (1995).

*

Mayr, H.: Geometry theorem proving package in SCRATCHPAT II: A primer. Tech. Rep. 88-1, RISC-Linz, Johannes Kepler Univ., Austria (1988).

*

McCallum, S.: Solving polynomial strict inequalities using cylindrical algebraic decomposition. Tech. Rep. 87-25, RISC-Linz, Johannes Kepler Univ., Austria (1987).

*

McDougal, T. F.: Diagrammatic reasoning in plane geometry. Preprint, Dept. of Comput. Sci., Univ. of Chicago, USA (1993).

*

McDougal, T. F.: Everyday reasoning meets geometry theorem-proving. In: Proc. AAAI-94 (Seattle, August 1-4, 1994), vol. 2, p. 1471.

*

McDougal, T. F., Hammond, K. J.: Representing and using procedural knowledge to build geometry proofs. In: Proc. AAAI-93 (Washington, D. C., August 18-20, 1993), pp. 60-65.

*

McPhee, N. F. Mechanically proving geometry theorems using Wu's method and Collins' method. Ph.D thesis, Univ. of Texas at Austin, USA (1993).

*

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

*

Mourrain, B., Stolfi, N.: Computational symbolic geometry. In: Invariant methods in discrete and computational geometry (White, N. L., ed.). Kluwer, Dordrecht, pp. 107-139 (1995).

*

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).

*

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

*

Ou, Z., Liu, J.: Variant geometry analysis and synthesis in mechanical CAD. In: Springer's LNAI 1669, pp. 275-285 (1999).

*

Owen, J.: Algebraic solution for geometry from dimensional constraints. In: Proc. ACM Symp. Solid Modeling Foundat. Appl. (Austin, June 5-7, 1991), pp. 397-407.

*

Padmanabhan, R., McCune, W.: Automated reasoning about cubic curves. Comput. Math. Appl. 29(2): 17-26 (1995).

*

Padmanabhan, R., McCune, W.: An equational characterization of the conic construction on cubic curves. Preprint MCS-P517-0595, Argonne National Laboratory, USA (1995).

*

Pfalzgraf, J.: A category of geometric spaces: Some computational aspects. Ann. Math. Artif. Intell. 13: 173-193 (1995).

*

Pfalzgraf, J.: On geometric and topological reasoning in robotics. Ann. Math. Artif. Intell. 19: 279-318 (1997).

*

Quaife, A.: Automated development of Tarski's geometry. J. Automat. Reason. 5: 97-118 (1989).

*

Recio, T., Sterk, H., Vélez, M. P.: Automatic geometry theorem proving. In: Some tapas of computer algebra (Cohen, A., Cuypers, H., Sterk, H., eds.), Springer, Berlin Heidelberg, pp. 276-296 (1999).

*

Recio, T., Vélez, M. P.: Automatic discovery of theorems in elementary geometry. J. Automat. Reason. 23: 63-82 (1999).

*

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.

*

Rege, A., Canny, J.: A practical algorithm for geometric theorem proving. In: Springer's LNCS 958, pp. 10-17 (1995).

*

Richter-Gebert, J.: Mechanical theorem proving in projective geometry. Ann. Math. Artif. Intell. 13: 139-172 (1995).

*

Roanes-Macías, E., Roanes-Lozano, E.: Automatic determination of geometric loci: 3D-extension of Simson-Steiner theorem. In: Springer's LNAI 1930, pp. 157-173 (2001).

*

Rouillier, F., Safey El Din, M., Schost, É.: Solving the Birkhoff interpolation problem via the critical point method: An experimental study. In: Springer's LNAI 2061, pp. 26-40 (2001).

*

Shi, H.: On the resultant formula for mechanical theorem proving. Math. Mech. Res. Preprints 4: 77-86 (1989).

*

Shi, H., Zou, F.: Flat central configurations of four planet motions. In: Springer's LNAI 1360, pp. 208-217 (1997).

*

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).

*

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

*

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.

*

Stokes, T., Bulmer, M.: A complex change of variables for geometrical reasoning. In: Springer's LNAI 2061, pp. 143-153 (2001).

*

Sturm, T., Weispfenning, V.: Computational geometry problems in REDLOG. In: Springer's LNAI 1360, pp. 58-86 (1997).

*

Sturmfels, B.: Computational synthetic geometry. Ph.D thesis, Univ. of Washington, USA (1987).

*

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.

*

Tran, Q.-N.: Extended Dixon's resultant and its applications. In: Springer's LNAI 1360, pp. 37-57 (1997).

*

Tulone, D., Yap, C., Li, C.: Randomized zero testing of radical expressions and elementary geometry theorem proving. In: Springer's LNAI 2061, pp. 58-82 (2001).

*

Ueberberg, J.: Interactive theorem proving and computer algebra. In: Springer's LNCS 958, pp. 1-9 (1995).

*

Ueberberg, J.: Interactive theorem proving and finite projective planes. In: Springer's LNCS 1138, pp. 274-288 (1996).

*

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

*

Wang, D.-K.: A mechanization proving of a group of space geometry problems. Math. Mech. Res. Preprints 5: 66-81 (1990).

*

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

*

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

*

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

*

Wang, D.: "Proving by examples" method and the inclusion of varieties. J. Syst. Sci. Math. Sci. 9: 40-46 (1989) [in Chinese].

*

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

*

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

*

Wang, D.: Some notes on algebraic methods for geometry theorem proving. Preprint (presented at Medlar 12-month Workshop, Schloß Weinberg, November 4-7, 1990), RISC-Linz, Johannes Kepler Univ., Austria (1990).

*

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

*

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), pp. 561-570.

*

Wang, D.: Algebraic factoring and geometry theorem proving. In: Springer's LNCS 814, pp. 386-400 (1994).

*

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).

*

Wang, D.: Elimination procedures for mechanical theorem proving in geometry. Ann. Math. Artif. Intell. 13: 1-24 (1995).

*

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

*

Wang, D.: GEOTHER: A geometry theorem prover. In: Springer's LNAI 1104, pp. 166-170 (1996).

*

Wang, D.: Geometry machines: From AI to SMC. In: Springer's LNCS 1138, pp. 213-239 (1996).

*

Wang, D.: Clifford algebraic calculus for geometric reasoning with application to computer vision. In: Springer's LNAI 1360, pp. 115-140 (1997).

*

Wang, D.: Gröbner bases applied to geometric theorem proving and discovering. In: Gröbner bases and applications (Buchberger, B., Winkler, F., eds.), Cambridge Univ. Press, Cambridge, pp. 281-301 (1998).

*

Wang, D.: Decomposing algebraic varieties. In: Springer's LNAI 1669, pp. 180-206 (1999).

*

Wang, D.: Geometric reasoning with geometric algebra. In: Advances in geometric algebra with applications (Bayro-Corrochano, E., Sobczyk, G., eds.), Birkhäuser, Boston, pp. 87-111 (2001).

*

Wang, D.: Automated generation of diagrams with Maple and Java. In: Algebra, geometry, and software systems (Joswig, M., Takayama, N., eds.), Springer, Berlin Heidelberg, pp. 277-287 (2003).

*

Wang, D., Gao, X.-S.: Geometry theorems proved mechanically using Wu's method - Part on Euclidean geometry. Math. Mech. Res. Preprints 2: 75-106 (1987).

*

Wang, D., Hu, S.: A mechanical proving system for constructible theorems in elementary geometry. J. Syst. Sci. Math. Sci. 7: 163-172 (1987) [in Chinese].

*

Wang, D., Zhi, L.: Algebraic factorization applied to geometric problems. In: Proc. ASCM '98 (Lanzhou, August 6-8, 1998), pp. 23-36.

*

Welham, B.: Geometry problem solving. Res. Paper 14, DAI, Univ. of Edinburgh, Scotland (1976).

*

Whiteley, W.: Analytic vs synthetic geometry for computers. In: Learning and geometry: Computational approaches (Kueker, D. W., Smith, C., eds.), Birkhäuser, Boston, pp. 121-141 (1996).

*

Whiteley, W.: Representing geometric objects. In: Learning and geometry: Computational approaches (Kueker, D. W., Smith, C., eds.), Birkhäuser, Boston, pp. 143-178 (1996).

*

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

*

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

*

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

*

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

*

Wu, T.-J.: On a collision problem. Math. Mech. Res. Preprints 7: 96-104 (1991).

*

Wu, W.-t.: On the decision problem and the mechanization of theorem-proving in elementary geometry. Sci. Sinica 21: 159-172 (1978). Also in: Automated theorem proving: After 25 years (Bledsoe, W. W., Loveland, D. W., eds.), AMS, Providence, pp. 213-234 (1984).

*

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

*

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.

*

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

*

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

*

Wu, W.-t.: Basic principles of mechanical theorem proving in elementary geometries. J. Syst. Sci. Math. Sci. 4: 207-235 (1984). Also in J. Automat. Reason. 2: 221-252 (1986).

*

Wu, W.-t.: Some recent advances in mechanical theorem-proving of geometries. In: Automated theorem proving: After 25 years (Bledsoe, W. W., Loveland, D. W., eds.), AMS, Providence, pp. 235-241 (1984).

*

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

*

Wu, W.-t.: A mechanization method of geometry and its applications I. J. Syst. Sci. Math. Sci. 6: 204-216 (1986).

*

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

*

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

*

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

*

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

*

Wu, W.-t.: A mechanization method of geometry and its applications III. Syst. Sci. Math. Sci. 1: 1-17 (1988).

*

Wu, W.-t.: Review and prospects of mechanical theorem proving. In: New advances in modern mathematics (Wu, W.-t., ed.), Anhui Sci & Tech Press, Hefei, pp. 181-188 (1988) [in Chinese].

*

Wu, W.-t.: A mechanization method of geometry and its applications IV. Syst. Sci. Math. Sci. 2: 97-109 (1989).

*

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.

*

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

*

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

*

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

*

Wu, W.-t.: On problems involving inequalities. Math. Mech. Res. Preprints 7: 1-13 (1992).

*

Wu, W.-t.: On a finiteness theorem about problems involving inequalities. Syst. Sci. Math. Sci. 7: 193-200 (1994).

*

Wu, W.-t.: Central configurations in planet motions and vortex motions. Math. Mech. Res. Preprints 13: 1-14 (1995).

*

Wu, W.-t.: Automatic geometry theorem-proving and automatic geometry problem-solving. In: Springer's LNAI 1669, pp. 1-13 (1999).

*

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

*

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.

*

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.

*

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.

*

Yang, H., Zhang, S., Feng, G.: Clifford algebra and mechanical geometry theorem proving. In: Proc. ASCM '98 (Lanzhou, August 6-8, 1998), pp. 49-63.

*

Yang, H., Zhang, S., Feng, G.: A Clifford algebraic method for geometric reasoning. In: Springer's LNAI 1669, pp. 111-129 (1999).

*

Yang, L.: On the area coordinates. In: Essays on elementary mathematics and education, Shanghai Education Press, Shanghai (1979).

*

Yang, L.: Computer-aided proving for new theorems of non-Euclidean geometry. Res. Rep. No. 4, Dept. of Math., The Australian National Univ., Australia (1989).

*

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).

*

Yang, L.: Practical automated reasoning on inequalities: Generic programs for inequality proving and discovering. In: Proc. ATCM98 (Tsukuba, August 24-28, 1998), pp. 36-44.

*

Yang, L., Fu, H., Zeng, Z.: A practical symbolic algorithm for the inverse kinematics of 6R manipulators with simple geometry. In: Springer's LNAI 1249, pp. 73-86 (1997).

*

Yang, L., Gao, X.-S., Chou, S.-C., Zhang, J.-Z.: Automated production of readable proofs for theorems in non-Euclidean geometries. In: Springer's LNAI 1360, pp. 171-188 (1997).

*

Yang, L., Hou, X., Xia, B.: Automated discovering and proving for geometric inequalities. In: Springer's LNAI 1669, pp. 30-46 (1999).

*

Yang, L., Xia, B.: Automated deduction in real geometry. In: Geometric computation (Chen, F., Wang, D., eds.), World Scientific, Singapore, pp. 248-298 (2003).

*

Yang, L., Zeng, Z.: Equi-Cevaline points of triangle. In: Proc. ASCM 2000 (Chiang Mai, December 17-21, 2000), pp. 130-137.

*

Yang, L., Zhang, J.: A practical program of automated proving for a class of geometric inequalities. In: Springer's LNAI 2061, pp. 41-57 (2001).

*

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).

*

Yang, L., Zhang, J.-Z., Hou, X.-R.: A criterion of dependency between algebraic equations and its applications. In: Proc. IWMM '92 (Beijing, July 16-18, 1992), pp. 110-134.

*

Yang, L., Zhang, J.-Z., Hou, X.-R.: A note on Wu Wen-tsün's nondegenerate condition. Chinese Sci. Bull. 38: 86-87 (1993). Also in: Computer mathematics (Tianjin, 1991), Nankai Ser. Pure Appl. Math. Theoret. Phys. 5, World Scientific, River Edge, pp. 127-135 (1993).

*

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.

*

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.

*

Zhang, J.-Z.: Points elimination methods for geometric problem solving. In: Mathematics mechanization and applications (Gao, X.-S., Wang, D., eds.), Academic Press, London, pp. 175-204 (2000).

*

Zhang, J.-Z., Chou, S.-C., Gao, X.-S.: Automated production of traditional proofs for theorems in Euclidean geometry I. Ann. Math. Artif. Intell. 13: 109-137 (1995).

*

Zhang, J.-Z., Li, C.: Automated reasoning in ICAI. In: Proc. ATCM98 (Tsukuba, August 24-28, 1998), pp. 36-44.

*

Zhang, J.-Z., Yang, L.: Principles of parallel numerical method and single-instance method of mechanical theorem proving. Math. Practice Theory 1: 34-43 (1989) [in Chinese].

*

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

*

Zhang, J.-Z., Yang, L., Gao, X.-S., Chou, S.-C.: Automated production of readable proofs for geometry theorems. Chinese J. Comput. 18(5): 380-393 (1995).

*

Zhang, J.-Z., Yang, L., Hou, X.-R.: A criterion for dependency of algebraic equations and its applications to automated theorem proving. In: Proc. Asian Math. Conf. (Hong Kong, 1990), pp. 548-553.

*

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

*

Zhang, J.-Z., Yang, L., Hou, X.-R.: The subresultant method for automated theorem proving in geometry. J. Syst. Sci. Math. Sci. 15: 10-15 (1995) [in Chinese].

*

Zhang, J.-Z., Yang, L., Hou, X.-R.: The WE complete algorithm for automated theorem proving in geometry. J. Syst. Sci. Math. Sci. 15: 200-207 (1995) [in Chinese].

Books    Articles    [A-B]    [C]    [D-J]    [K-V]    [W]    [X-Z]

Welcome to visit and refer to this web page.

• If you find errors and/or incomplete data in the bibliography, please let me know, and I will correct them.
• If you have written or know some other articles published on the subject, please send me a note, and I will add them to the list.
• Your help on disseminating this information by including a link in your web page is highly appreciated.