Bibliography on Geometric
Reasoning
Readme
Articles
[A-B]
[C]
[D-J]
[K-V]
[W]
[X-Z]
-
- *
- 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].
- *
- 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.
Maintained by Dongming Wang -
Copyright © 1998-2003. All rights reserved.
Last Modification: October 6, 2003