{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,20]],"date-time":"2026-07-20T15:17:36Z","timestamp":1784560656195,"version":"3.55.0"},"publisher-location":"Berlin, Heidelberg","reference-count":171,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540617327","type":"print"},{"value":"9783540707400","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61732-9_60","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T22:16:40Z","timestamp":1330294600000},"page":"213-239","source":"Crossref","is-referenced-by-count":14,"title":["Geometry machines: From AI to SMC"],"prefix":"10.1007","author":[{"given":"Dongming","family":"Wang","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"key":"14_CR1","unstructured":"Anderson, J. R.: Tuning of search of the problem space for geometry proofs. In: Proc. IJCAI '81 (Vancouver, August 24\u201328, 1981), pp. 165\u2013170."},{"key":"14_CR2","unstructured":"Anderson, J. R., Boyle, C. F., Yost, G.: The geometry tutor. In: Proc. IJCAI '85 (Los Angeles, August 18\u201323, 1985), pp. 1\u20137."},{"key":"14_CR3","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1016\/0004-3702(88)90049-5","volume":"37","author":"D. S. Arnon","year":"1988","unstructured":"Arnon, D. S.: Geometric reasoning with logic and algebra. Artif. Intell. 37: 37\u201360 (1988).","journal-title":"Artif. Intell."},{"key":"14_CR4","first-page":"95","volume":"850","author":"P. Balbiani","year":"1994","unstructured":"Balbiani, P.: Equation solving in projective planes and planar ternary rings. In: LNCS 850, pp. 95\u2013113 (1994).","journal-title":"LNCS"},{"key":"14_CR5","first-page":"31","volume":"968","author":"P. Balbiani","year":"1995","unstructured":"Balbiani, P.: Equation solving in geometrical theories. In: LNCS 968, pp. 31\u201355 (1995).","journal-title":"LNCS"},{"key":"14_CR6","volume-title":"El\u00e9ments de g\u00e9om\u00e9trie m\u00e9canique","author":"P. Balbiani","year":"1994","unstructured":"Balbiani, P., Dugat, V., Fari\u00f1as del Cerro, L., Lopez, A.: El\u00e9ments de g\u00e9om\u00e9trie m\u00e9canique. Herm\u00e8s, Paris (1994)."},{"key":"14_CR7","first-page":"196","volume":"909","author":"P. Balbiani","year":"1995","unstructured":"Balbiani, P., Fari\u00f1as del Cerro, L.: Affine geometry of collinearity and conditional term rewriting. In: LNCS 909, pp. 196\u2013213 (1995).","journal-title":"LNCS"},{"key":"14_CR8","unstructured":"Balbiani, P., Lopez, A.: Simplification des figures de la g\u00e9om\u00e9trie affine plane d'incidence. In: 9e congr\u00e8s reconnaissance des formes et intell. artif. (Paris, January 11\u201314, 1994), pp. 341\u2013351."},{"key":"14_CR9","series-title":"Comptemp. Math. 29","volume-title":"Automated theorem proving: After 25 years","year":"1984","unstructured":"Bledsoe, W. W., Loveland, D. W. (eds.): Automated theorem proving: After 25 years. Comptemp. Math. 29, Amer. Math. Soc., Providence (1984)."},{"key":"14_CR10","volume-title":"Geometry and robotics","year":"1988","unstructured":"Boissonnat, J.-D., Laumond, J.-P. (eds.): Geometry and robotics. Springer, Berlin-Heidelberg (1988)."},{"key":"14_CR11","first-page":"232","volume":"333","author":"B. Br\u00fcderlin","year":"1988","unstructured":"Br\u00fcderlin, B.: Automatizing geometric proofs and constructions. In: LNCS 333, pp. 232\u2013252 (1988).","journal-title":"LNCS"},{"key":"14_CR12","doi-asserted-by":"crossref","first-page":"184","DOI":"10.1007\/978-94-009-5225-6_6","volume-title":"Multidimensional systems theory","author":"B. Buchberger","year":"1985","unstructured":"Buchberger, B.: Gr\u00f6bner bases: An algorithmic method in polynomial ideal theory. In: Multidimensional systems theory (Bose, N. K., ed.), Reidel, Dordrecht-Boston, pp. 184\u2013232 (1985)."},{"key":"14_CR13","first-page":"59","volume-title":"Mathematical aspects of scientific software","author":"B. Buchberger","year":"1987","unstructured":"Buchberger, B.: Applications of Gr\u00f6bner bases in non-linear computational geometry. In: Mathematical aspects of scientific software (Rice, J. R., ed.), Springer, New York, pp. 59\u201387 (1987)."},{"key":"14_CR14","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1146\/annurev.cs.03.060188.000505","volume":"3","author":"B. Buchberger","year":"1988","unstructured":"Buchberger, B., Collins, G. E., Kutzler, B.: Algebraic methods for geometric reasoning. Ann. Rev. Comput. Sci. 3: 85\u2013119 (1988).","journal-title":"Ann. Rev. Comput. Sci."},{"key":"14_CR15","first-page":"217","volume":"19","author":"R. Caferra","year":"1995","unstructured":"Caferra, R., Herment, M.: A generic graphic framework for combining inference tools and editing proofs and formulae. JSC 19: 217\u2013243 (1995).","journal-title":"JSC"},{"key":"14_CR16","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1007\/BF00245819","volume":"6","author":"G. Carr\u00e0 Ferro","year":"1990","unstructured":"Carr\u00e0 Ferro, G., Gallo, G.: A procedure to prove statements in differential geometry. JAR 6: 203\u2013209 (1990).","journal-title":"JAR"},{"key":"14_CR17","doi-asserted-by":"crossref","first-page":"351","DOI":"10.1007\/BF00885765","volume":"12","author":"G. Carr\u00e0 Ferro","year":"1994","unstructured":"Carr\u00e0 Ferro, G.: An extension of a procedure to prove statements in differential geometry. JAR 12: 351\u2013358 (1994).","journal-title":"JAR"},{"key":"14_CR18","first-page":"895","volume":"76","author":"E. Cerutti","year":"1969","unstructured":"Cerutti, E., Davis, P. J.: Formac meets Pappus: Some observations on elementary analytic geometry by computer. Amer. Math. Monthly 76: 895\u2013905 (1969).","journal-title":"Amer. Math. Monthly"},{"key":"14_CR19","series-title":"Comptemp. Math. 29","doi-asserted-by":"crossref","first-page":"243","DOI":"10.1090\/conm\/029\/14","volume-title":"Automated theorem proving: After 25 years","author":"S.-C. Chou","year":"1984","unstructured":"Chou, S.-C.: Proving elementary geometry theorems using Wu's algorithm. In [9], pp. 243\u2013286 (1984)."},{"key":"14_CR20","first-page":"679","volume":"230","author":"S.-C. Chou","year":"1986","unstructured":"Chou, S.-C.: GEO-prover \u2014 A geometry theorem prover developed at UT. In: LNCS 230, pp. 679\u2013680 (1986).","journal-title":"LNCS"},{"key":"14_CR21","first-page":"291","volume":"3","author":"S.-C. Chou","year":"1987","unstructured":"Chou, S.-C.: A method for the mechanical derivation of formulas in elementary geometry. JAR 3: 291\u2013299 (1987).","journal-title":"JAR"},{"key":"14_CR22","volume-title":"Mechanical geometry theorem proving","author":"S.-C. Chou","year":"1988","unstructured":"Chou, S.-C.: Mechanical geometry theorem proving. Reidel, Dordrecht-Boston (1988)."},{"key":"14_CR23","doi-asserted-by":"crossref","unstructured":"Chou, S.-C.: Automated reasoning in geometries using the characteristic set method and Gr\u00f6bner basis method. In: Proc. ISSAC '90 (Tokyo, August 20\u201324, 1990), pp. 255\u2013260.","DOI":"10.1145\/96877.96942"},{"key":"14_CR24","first-page":"687","volume":"607","author":"S.-C. Chou","year":"1992","unstructured":"Chou, S.-C.: A geometry theorem prover for Macintoshes. In: LNCS 607, pp. 687\u2013690 (1992).","journal-title":"LNCS"},{"key":"14_CR25","doi-asserted-by":"crossref","unstructured":"Chou, S.-C., Gao, X.-S.: Mechanical formula derivation in elementary geometries. In: Proc. ISSAC '90 (Tokyo, August 20\u201324, 1990), pp. 265\u2013270.","DOI":"10.1145\/96877.96946"},{"key":"14_CR26","first-page":"207","volume":"449","author":"S.-C. Chou","year":"1990","unstructured":"Chou, S.-C., Gao, X.-S.: Ritt-Wu's decomposition algorithm and geometry theorem proving. In: LNCS 449, pp. 207\u2013220 (1990).","journal-title":"LNCS"},{"key":"14_CR27","first-page":"20","volume":"607","author":"S.-C. Chou","year":"1992","unstructured":"Chou, S.-C., Gao, X.-S.: Proving geometry statements of constructive type. In: LNCS 607, pp. 20\u201334 (1992).","journal-title":"LNCS"},{"key":"14_CR28","first-page":"1","volume-title":"Automated reasoning","author":"S.-C. Chou","year":"1992","unstructured":"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\u201312 (1992)."},{"key":"14_CR29","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1007\/BF00881834","volume":"10","author":"S.-C. Chou","year":"1993","unstructured":"Chou, S.-C., Gao, X.-S.: Automated reasoning in differential geometry and mechanics using the characteristic set method \u2014 Parts I, II. JAR 10: 161\u2013189 (1993).","journal-title":"JAR"},{"key":"14_CR30","first-page":"186","volume":"6","author":"S.-C. Chou","year":"1993","unstructured":"Chou, S.-C., Gao, X.-S.: Automated reasoning in differential geometry and mechanics using the characteristic method IV. SSMS 6: 186\u2013192 (1993).","journal-title":"SSMS"},{"key":"14_CR31","first-page":"139","volume-title":"Issues in robotics and nonlinear geometry","author":"S.-C. Chou","year":"1992","unstructured":"Chou, S.-C., Gao, X.-S., Arnon, D. S.: On the mechanical proof of geometry theorems involving inequalities. In: Issues in robotics and nonlinear geometry (Hoffmann, C., ed.), JAI Press, Greenwich, pp. 139\u2013181 (1992)."},{"key":"14_CR32","volume-title":"Tech. Rep. TR-WSU-94-9","author":"S.-C. Chou","year":"1994","unstructured":"Chou, S.-C., Gao, X.-S., Yang, L., Zhang, J.-Z.: Automated production of readable proofs for theorems in non-Euclidean geometries. Tech. Rep. TR-WSU-94-9, Wichita State Univ., USA (1994)."},{"key":"14_CR33","doi-asserted-by":"crossref","unstructured":"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\u201323, 1993), pp. 48\u201356.","DOI":"10.1109\/LICS.1993.287601"},{"key":"14_CR34","doi-asserted-by":"crossref","unstructured":"Chou, S.-C., Gao, X.-S., Zhang, J.-Z.: Automated geometry theorem proving by vector calculation. In: Proc. ISSAC '93 (Kiev, July 6\u20138, 1993), pp. 284\u2013291.","DOI":"10.1145\/164081.164142"},{"key":"14_CR35","doi-asserted-by":"crossref","DOI":"10.1142\/2196","volume-title":"Machine proofs in geometry","author":"S.-C. Chou","year":"1994","unstructured":"Chou, S.-C., Gao, X.-S., Zhang, J.-Z.: Machine proofs in geometry. World Scientific, Singapore (1994)."},{"key":"14_CR36","doi-asserted-by":"crossref","first-page":"257","DOI":"10.1007\/BF00881858","volume":"14","author":"S.-C. Chou","year":"1995","unstructured":"Chou, S.-C., Gao, X.-S., Zhang, J.-Z.: Automated production of traditional proofs in solid geometry. JAR 14: 257\u2013291 (1995).","journal-title":"JAR"},{"key":"14_CR37","unstructured":"Chou, S.-C., Ko, H.-P.: On mechanical theorem proving in Minkowskian plane geometry. In: Proc. IEEE Symp. LICS (Cambridge, June 16\u201318, 1986), pp. 187\u2013192."},{"key":"14_CR38","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1007\/BF02328448","volume":"2","author":"S.-C. Chou","year":"1986","unstructured":"Chou, S.-C., Schelter, W. F.: Proving geometry theorems with rewrite rules. JAR 2: 253\u2013273 (1986).","journal-title":"JAR"},{"key":"14_CR39","first-page":"33","volume-title":"Resolution of equations in algebraic structures","author":"S.-C. Chou","year":"1989","unstructured":"Chou, S.-C., Schelter, W. F., Yang, J.-G.: Characteristic sets and Gr\u00f6bner bases in geometry theorem proving. In: Resolution of equations in algebraic structures (A\u00eft-Kaaci, H., Nivat, M., eds.), Academic Press, San Diego, pp. 33\u201392 (1989)."},{"key":"14_CR40","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/BF01840382","volume":"5","author":"S.-C. Chou","year":"1990","unstructured":"Chou, S.-C., Schelter, W. F., Yang, J.-G.: An algorithm for constructing Gr\u00f6bner bases from characteristic sets and its application to geometry. Algorithmica 5: 147\u2013154 (1990).","journal-title":"Algorithmica"},{"key":"14_CR41","doi-asserted-by":"crossref","first-page":"237","DOI":"10.1007\/BF01553889","volume":"4","author":"S.-C. Chou","year":"1989","unstructured":"Chou, S.-C., Yang, J. G.: On the algebraic formulation of certain geometry statements and mechanical geometry theorem proving. Algorithmica 4: 237\u2013262 (1989).","journal-title":"Algorithmica"},{"key":"14_CR42","volume-title":"Laborat\u00f3rio Nacional de Engenhaaria Civil Mem\u00f3ria no. 525","author":"H. Coelho","year":"1979","unstructured":"Coelho, H., Pereira, L. M.: GEOM: A Prolog geometry theorem prover. Laborat\u00f3rio Nacional de Engenhaaria Civil Mem\u00f3ria no. 525, Ministerio de Habitacao e Obrass Publicas, Portugal (1979)."},{"key":"14_CR43","doi-asserted-by":"crossref","first-page":"329","DOI":"10.1007\/BF00248249","volume":"2","author":"H. Coelho","year":"1986","unstructured":"Coelho, H., Pereira, L. M.: Automated reasoning in geometry theorem proving with Prolog. JAR 2: 329\u2013390 (1986).","journal-title":"JAR"},{"key":"14_CR44","first-page":"134","volume":"33","author":"G. E. Collins","year":"1975","unstructured":"Collins, G. E.: Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In: LNCS 33, pp. 134\u2013165 (1975).","journal-title":"LNCS"},{"key":"14_CR45","first-page":"183","volume":"948","author":"P. Conti","year":"1995","unstructured":"Conti, P., Traverso, C.: A case of automatic theorem proving in Euclidean geometry: The Maclane 83 theorem. In: LNCS 948, pp. 183\u2013193 (1995).","journal-title":"LNCS"},{"key":"14_CR46","volume-title":"Computer-aided geometric reasoning","year":"1987","unstructured":"Crapo, H. (ed.): Computer-aided geometric reasoning. Proc. INRIA Workshop (INRIA Sophia-Antipolis, June 22\u201326, 1987), INRIA Rocquencourt, France."},{"key":"14_CR47","first-page":"770","volume":"310","author":"D. A. Cyrluk","year":"1988","unstructured":"Cyrluk, D. A., Harris, R. M., Kapur, D.: GEOMETER: A theorem prover for algebraic geometry. In: LNCS 310, pp. 770\u2013771 (1988).","journal-title":"LNCS"},{"key":"14_CR48","doi-asserted-by":"crossref","unstructured":"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\u20135, 1994), pp. 329\u2013336.","DOI":"10.1109\/MFI.1994.398436"},{"key":"14_CR49","first-page":"1066","volume":"34","author":"M.-K. Deng","year":"1989","unstructured":"Deng, M.-K.: The parallel numerical method of proving the constructive geometric theorem. Chinese Sci. Bull. 34: 1066\u20131070 (1989).","journal-title":"Chinese Sci. Bull."},{"key":"14_CR50","first-page":"11","volume":"8","author":"E. W. Elcock","year":"1977","unstructured":"Elcock, E. W.: Representation of knowledge in a geometry machine. Machine Intell. 8: 11\u201329 (1977).","journal-title":"Machine Intell."},{"key":"14_CR51","first-page":"27","volume-title":"Resolution of equations in algebraic structures","author":"D. Fearnley-Sander","year":"1989","unstructured":"Fearnley-Sander, D.: The idea of a diagram. In: Resolution of equations in algebraic structures (A\u00eft-Kaaci, H., Nivat, M., eds.), Academic Press, San Diego, pp. 27\u2013150 (1989)."},{"key":"14_CR52","unstructured":"Fevre, S.: A hybrid method for proving theorems in elementary geometry. In: Proc. ASCM '95 (Beijing, August 18\u201320, 1995), pp. 113\u2013123."},{"key":"14_CR53","first-page":"403","volume":"6","author":"X.-S. Gao","year":"1990","unstructured":"Gao, X.-S.: Transcendental functions and mechanical theorem proving in elementary geometries. JAR 6: 403\u2013417 (1990).","journal-title":"JAR"},{"key":"14_CR54","first-page":"263","volume":"5","author":"X.-S. Gao","year":"1992","unstructured":"Gao, X.-S.: Transformation theorems among Cayley-Klein geometries. SSMS 5: 263\u2013273 (1992).","journal-title":"SSMS"},{"key":"14_CR55","doi-asserted-by":"crossref","unstructured":"Gao, X.-S., Chou, S.-C.: Computations with parametric equations. In: Proc. ISSAC '91 (Bonn, July 15\u201317, 1991), pp. 122\u2013127.","DOI":"10.1145\/120694.120710"},{"key":"14_CR56","unstructured":"Gao, X.-S., Li, Y.-L., Lin, D.-D., L\u00fc, X.-S.: A geometric theorem prover based on Wu's method. In: Proc. IWMM '92 (Beijing, July 16\u201318, 1992), pp. 201\u2013205."},{"key":"14_CR57","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1007\/BF01224042","volume":"53","author":"X.-S. Gao","year":"1995","unstructured":"Gao, X.-S., Wang, D.-K.: On the automatic derivation of a set of geometric formulae. J. Geom. 53: 79\u201388 (1995).","journal-title":"J. Geom."},{"key":"14_CR58","unstructured":"Gelernter, H.: Realization of a geometry theorem proving machine. In: Proc. Int. Conf. Info. Process. (Paris, June 15\u201320, 1959), pp. 273\u2013282."},{"key":"14_CR59","unstructured":"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\u20135, 1960), pp. 143\u2013147."},{"key":"14_CR60","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1016\/0004-3702(70)90005-6","volume":"1","author":"P. C. Gilmore","year":"1970","unstructured":"Gilmore, P. C.: An examination of the geometry theorem machine. Artif. Intell. 1: 171\u2013187 (1970).","journal-title":"Artif. Intell."},{"key":"14_CR61","volume-title":"MIT AI Memo no. 28","author":"I. Goldstein","year":"1973","unstructured":"Goldstein, I.: Elementary geometry theorem proving. MIT AI Memo no. 28, MIT, USA (1973)."},{"key":"14_CR62","doi-asserted-by":"crossref","unstructured":"Guergueb, A., Mainguen\u00e9, J., Roy, M.-F.: Examples of automatic theorem proving in real geometry. In: Proc. ISSAC '94 (Oxford, July 20\u201322, 1994), pp. 20\u201324.","DOI":"10.1145\/190347.190354"},{"key":"14_CR63","doi-asserted-by":"crossref","unstructured":"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\u201323, 1986), pp. 141\u2013147.","DOI":"10.1145\/32439.32468"},{"key":"14_CR64","first-page":"579","volume":"11","author":"T. F. Havel","year":"1991","unstructured":"Havel, T. F.: Some examples of the use of distances as coordinates for Euclidean geometry. JSC 11: 579\u2013593 (1991).","journal-title":"JSC"},{"key":"14_CR65","volume-title":"Grundlagen der Geometrie","author":"D. Hilbert","year":"1899","unstructured":"Hilbert, D.: Grundlagen der Geometrie. Teubner, Stuttgart (1899)."},{"key":"14_CR66","series-title":"Ann. Math. Artif. Intell. 13","volume-title":"Algebraic approaches to geometric reasoning","year":"1995","unstructured":"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)."},{"key":"14_CR67","first-page":"824","volume":"29","author":"J. Hong","year":"1986","unstructured":"Hong, J.: Can we prove geometry theorems by computing an example? Sci. Sinica 29: 824\u2013834 (1986).","journal-title":"Sci. Sinica"},{"key":"14_CR68","doi-asserted-by":"crossref","unstructured":"Hong, J.: Proving by example and gap theorems. In: Proc. 27th Ann. Symp. Foundations Comput. Sci. (Toronto, October 27\u201329, 1986), pp. 107\u2013116.","DOI":"10.1109\/SFCS.1986.48"},{"key":"14_CR69","first-page":"56","volume":"5","author":"M. A. Hussain","year":"1986","unstructured":"Hussain, M. A., Drew, M. A., Noble, B.: Using a computer for automatic proving of geometric theorems. Comput. Mech. Eng. 5: 56\u201369 (1986).","journal-title":"Comput. Mech. Eng."},{"key":"14_CR70","series-title":"Ann. Math. Artif. Intell. 13(1,2)","first-page":"73","volume-title":"Algebraic approaches to geometric reasoning","author":"M. Kalkbrener","year":"1995","unstructured":"Kalkbrener, M.: A generalized Euclidean algorithm for geometry theorem proving. In [66]: 73\u201395 (1995)."},{"key":"14_CR71","first-page":"1","volume":"9","author":"A. Kandri-Rody","year":"1990","unstructured":"Kandri-Rody, A., Weispfenning, V.: Non-commutative Gr\u00f6bner bases in algebras of solvable type. JSC 9: 1\u201326 (1990).","journal-title":"JSC"},{"key":"14_CR72","doi-asserted-by":"crossref","unstructured":"Kapur, D.: Geometry theorem proving using Hilbert's Nullstellensatz. In: Proc. SYMSAC '86 (Waterloo, July 21\u201323, 1986), pp. 202\u2013208.","DOI":"10.1145\/32439.32479"},{"key":"14_CR73","first-page":"399","volume":"2","author":"D. Kapur","year":"1986","unstructured":"Kapur, D.: Using Gr\u00f6bner bases to reason about geometry problems. JSC 2: 399\u2013408 (1986).","journal-title":"JSC"},{"key":"14_CR74","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1016\/0004-3702(88)90050-1","volume":"37","author":"D. Kapur","year":"1988","unstructured":"Kapur, D.: A refutational approach to geometry theorem proving. Artif. Intell. 37: 61\u201393 (1988).","journal-title":"Artif. Intell."},{"key":"14_CR75","doi-asserted-by":"crossref","first-page":"15","DOI":"10.1016\/0004-3702(88)90048-3","volume":"37","author":"D. Kapur","year":"1988","unstructured":"Kapur, D., Mundy, J. L.: Wu's method and its application to perspective viewing. Artif. Intell. 37: 15\u201326 (1988).","journal-title":"Artif. Intell."},{"key":"14_CR76","series-title":"Artif. Intell. 37","volume-title":"Geometric reasoning","year":"1989","unstructured":"Kapur, D., Mundy, J. L. (eds.): Geometric reasoning. Special issue of Artif. Intell. 37, The MIT Press, Cambridge (1989)."},{"key":"14_CR77","doi-asserted-by":"crossref","unstructured":"Kapur, D., Saxena, T., Yang, L.: Algebraic and geometric reasoning using Dixon resultants. In: Proc. ISSAC '94 (Oxford, July 20\u201322, 1994), pp. 99\u2013107.","DOI":"10.1145\/190347.190372"},{"key":"14_CR78","doi-asserted-by":"crossref","unstructured":"Kapur, D., Wan, H. K.: Refutational proofs of geometry theorems via characteristic set computation. In: Proc. ISSAC '90 (Tokyo, August 20\u201324, 1990), pp. 277\u2013284.","DOI":"10.1145\/96877.96949"},{"issue":"4","key":"14_CR79","first-page":"60","volume":"4","author":"T. J. Kelanic","year":"1978","unstructured":"Kelanic, T. J.: Theorem-proving with EUCLID. Creative Comput. 4\/4: 60\u201363 (1978).","journal-title":"Creative Comput."},{"key":"14_CR80","volume-title":"Tech. Rep. 86CRD-081","author":"H.-P. Ko","year":"1986","unstructured":"Ko, H.-P.: ALGE-prover II: A new edition of ALGE-prover. Tech. Rep. 86CRD-081, General Electric Co., Schenectady, USA (1986)."},{"key":"14_CR81","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1016\/0004-3702(88)90051-3","volume":"37","author":"H.-P. Ko","year":"1988","unstructured":"Ko, H.-P.: Geometry theorem proving by decomposition of quasi-algebraic sets: An application of the Ritt-Wu principle. Artif. Intell. 37: 95\u2013122 (1988).","journal-title":"Artif. Intell."},{"key":"14_CR82","doi-asserted-by":"crossref","first-page":"709","DOI":"10.1216\/RMJ-1989-19-3-709","volume":"19","author":"H.-P. Ko","year":"1989","unstructured":"Ko, H.-P., Chou, S.-C.: A decision method for certain algebraic geometry problems. Rocky Mountain J. Math. 19: 709\u2013724 (1989).","journal-title":"Rocky Mountain J. Math."},{"key":"14_CR83","first-page":"225","volume":"48","author":"H.-P. Ko","year":"1985","unstructured":"Ko, H.-P., Hussain, M. A.: A study of Wu's method \u2014 A method to prove certain theorems in elementary geometry. Congr. Numer. 48: 225\u2013242 (1985).","journal-title":"Congr. Numer."},{"key":"14_CR84","volume-title":"Tech. Rep. 85CRD139","author":"H.-P. Ko","year":"1985","unstructured":"Ko, H.-P., Hussain, M. A.: ALGE-prover: An algebraic geometry theorem proving software. Tech. Rep. 85CRD139, General Electric Co., Schenectady, USA (1985)."},{"key":"14_CR85","first-page":"246","volume":"387","author":"K. Kusche","year":"1989","unstructured":"Kusche, K., Kutzler, B., Stifter, S.: Implementation of a geometry theorem proving package in Scratchpad II. In: LNCS 387, pp. 246\u2013257 (1989).","journal-title":"LNCS"},{"key":"14_CR86","volume-title":"Ph.D thesis","author":"B. Kutzler","year":"1988","unstructured":"Kutzler, B.: Algebraic approaches to automated geometry theorem proving. Ph.D thesis, RISC-LINZ, Johannes Kepler Univ., Austria (1988)."},{"key":"14_CR87","doi-asserted-by":"crossref","unstructured":"Kutzler, B.: Careful algebraic translations of geometry theorems. In: Proc. ISSAC '89 (Portland, July 17\u201319, 1989), pp. 254\u2013263.","DOI":"10.1145\/74540.74572"},{"key":"14_CR88","doi-asserted-by":"crossref","unstructured":"Kutzler, B., Stifter, S.: Automated geometry theorem proving using Buchberger's algorithm. In: Proc. SYMSAC '86 (Waterloo, July 21\u201323, 1986), pp. 209\u2013214.","DOI":"10.1145\/32439.32480"},{"key":"14_CR89","first-page":"389","volume":"2","author":"B. Kutzler","year":"1986","unstructured":"Kutzler, B., Stifter, S.: On the application of Buchberger's algorithm to automated geometry theorem proving. JSC 2: 389\u2013397 (1986).","journal-title":"JSC"},{"key":"14_CR90","first-page":"693","volume":"230","author":"B. Kutzler","year":"1986","unstructured":"Kutzler, B., Stifter, S.: A geometry theorem prover based on Buchberger's algorithm. In: LNCS 230, pp. 693\u2013694 (1986).","journal-title":"LNCS"},{"key":"14_CR91","volume-title":"Tech. Rep. 86-12","author":"B. Kutzler","year":"1986","unstructured":"Kutzler, B., Stifter, S.: Collection of computerized proofs of geometry theorems. Tech. Rep. 86-12, RISC-LINZ, Johannes Kepler Univ., Austria (1986)."},{"key":"14_CR92","volume-title":"Intelligent learning environments \u2014 The case of geometry","year":"1996","unstructured":"Laborde, J.-M. (ed.): Intelligent learning environments \u2014 The case of geometry. Springer, Berlin-New York (1996)."},{"key":"14_CR93","first-page":"37","volume-title":"Mathematics-Mechanization Research Preprints, no. 14","author":"H. Li","year":"1996","unstructured":"Li, H.: Clifford algebra and area method. In [99]: 37\u201369 (1996)."},{"key":"14_CR94","volume-title":"Proving theorems in elementary geometry with Clifford algebraic method","author":"H. Li","year":"1995","unstructured":"Li, H., Cheng, M.: Proving theorems in elementary geometry with Clifford algebraic method. Preprint, MMRC, Academia Sinica, China (1995)."},{"key":"14_CR95","first-page":"54","volume-title":"Mathematics-Mechanization Research Preprints, no. 4","author":"Z. Li","year":"1989","unstructured":"Li, Z.: Automatic implicitization of parametric objects. In [99]: 54\u201362 (1989)."},{"key":"14_CR96","series-title":"Ann. Math. Artif. Intell. 13","first-page":"25","volume-title":"Algebraic approaches to geometric reasoning","author":"Z. Li","year":"1995","unstructured":"Li, Z.: Mechanical theorem proving in the local theory of surfaces. In [66]: 25\u201346 (1995)."},{"key":"14_CR97","doi-asserted-by":"crossref","unstructured":"Lin, D., Liu, Z.: Some results on theorem proving in geometry over finite fields. In: Proc. ISSAC '93 (Kiev, July 6\u20138, 1993), pp. 292\u2013300.","DOI":"10.1145\/164081.164143"},{"key":"14_CR98","first-page":"401","volume":"814","author":"N. F. McPhee","year":"1994","unstructured":"McPhee, N. F., Chou, S.-C., Gao, X.-S.: Mechanically proving geometry theorems using a combination of Wu's method and Collins' method. In: LNCS 814, pp. 401\u2013415 (1994).","journal-title":"LNCS"},{"key":"14_CR99","volume-title":"Mathematics-Mechanization Research Preprints, nos. 1\u201314","year":"1987\u20131996","unstructured":"MMRC (ed.): Mathematics-Mechanization Research Preprints, nos. 1\u201314. Academia Sinica, China (1987\u20131996)."},{"key":"14_CR100","first-page":"117","volume-title":"Reasoning about 3-D space with algebraic deduction","author":"J. L. Mundy","year":"1986","unstructured":"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\u2013124 (1986)."},{"key":"14_CR101","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0004-3702(75)90013-2","volume":"6","author":"A. J. Nevins","year":"1975","unstructured":"Nevins, A. J.: Plane geometry theorem proving using forward chaining. Artif. Intell. 6: 1\u201323 (1975).","journal-title":"Artif. Intell."},{"key":"14_CR102","series-title":"Ann. Math. Artif. Intell. 13(1,2)","first-page":"173","volume-title":"Algebraic approaches to geometric reasoning","author":"J. Pfalzgraf","year":"1995","unstructured":"Pfalzgraf, J.: A category of geometric spaces: Some computational aspects. In [66]: 173\u2013193 (1995)."},{"key":"14_CR103","volume-title":"The robotics benchmark","author":"J. Pfalzgraf","year":"1990","unstructured":"Pfalzgraf, J., Stokkermans, K., Wang, D.: The robotics benchmark. In: Proc. 12-Month MEDLAR Workshop (Weinberg Castle, November 4\u20137, 1990), DOC, Imperial College, Univ. of London, England."},{"key":"14_CR104","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1007\/BF00245024","volume":"5","author":"A. Quaife","year":"1989","unstructured":"Quaife, A.: Automated development of Tarski's geometry. JAR 5: 97\u2013118 (1989).","journal-title":"JAR"},{"key":"14_CR105","doi-asserted-by":"crossref","unstructured":"Rege, A.: A complete and practical algorithm for geometric theorem proving. In: Proc. 11th Ann. Symp. Comput. Geom. (Vancouver, June 5\u20137, 1995), pp. 277\u2013286.","DOI":"10.1145\/220279.220309"},{"key":"14_CR106","series-title":"Ann. Math. Artif. Intell. 13(1,2)","first-page":"139","volume-title":"Algebraic approaches to geometric reasoning","author":"J. Richter-Gebert","year":"1995","unstructured":"Richter-Gebert, J.: Mechanical theorem proving in projective geometry. In [66]: 139\u2013172 (1995)."},{"key":"14_CR107","volume-title":"Differential algebra","author":"J. F. Ritt","year":"1950","unstructured":"Ritt, J. F.: Differential algebra. Amer. Math. Soc., New York (1950)."},{"key":"14_CR108","first-page":"77","volume-title":"Mathematics-Mechanization Research Preprints, no. 4","author":"H. Shi","year":"1989","unstructured":"Shi, H.: On the resultant formula for mechanical theorem proving. In [99]: 77\u201386 (1989)."},{"key":"14_CR109","volume-title":"RAPPORT de DEA","author":"F. Smietanski","year":"1986\/87","unstructured":"Smietanski, F.: Syst\u00e8mes de r\u00e9\u00e9criture sur des id\u00e8aux de polyn\u00f4mes, g\u00e9om\u00e9trie et calcul formel. RAPPORT de DEA, E.N.S., Universit\u00e9 de Jussieu Paris 7, France (1986\/87)."},{"key":"14_CR110","unstructured":"Starkey, J. D.: EUCLID: A program which conjectures, proves and evaluates theorems in elementary geometry. Order no. 75-2780, Univ. Microfilms (1975)."},{"key":"14_CR111","doi-asserted-by":"crossref","unstructured":"Stifter, S.: Geometry theorem proving in vector spaces by means of Gr\u00f6bner bases. In: Proc. ISSAC '93 (Kiev, July 6\u20138, 1993), pp. 301\u2013310.","DOI":"10.1145\/164081.164144"},{"key":"14_CR112","doi-asserted-by":"crossref","unstructured":"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\u201310, 1986), pp. 280\u2013285.","DOI":"10.1109\/ROBOT.1986.1087691"},{"key":"14_CR113","volume-title":"A decision method for elementary algebra and geometry","author":"A. Tarski","year":"1948","unstructured":"Tarski, A.: A decision method for elementary algebra and geometry. The RAND Corporation, Santa Monica (1948)."},{"key":"14_CR114","first-page":"1","volume":"958","author":"J. Ueberberg","year":"1995","unstructured":"Ueberberg, J.: Interactive theorem proving and computer algebra. In: LNCS 958, pp. 1\u20139 (1995).","journal-title":"LNCS"},{"key":"14_CR115","volume-title":"AI Lab Memo no. 321","author":"S. Ullmen","year":"1975","unstructured":"Ullmen, S.: A model-driven geometry theorem prover. AI Lab Memo no. 321, MIT, Cambridge, USA (1975)."},{"key":"14_CR116","unstructured":"Wang, D.-K.: Mechanical solution of a group of space geometry problems. In: Proc. IWMM '92 (Beijing, July 16\u201318, 1992), pp. 236\u2013243."},{"key":"14_CR117","volume-title":"Ph.D thesis","author":"D. Wang","year":"1987","unstructured":"Wang, D.: Mechanical approach for polynomial set and its related fields. Ph.D thesis, Academia Sinica, China (1987) [in Chinese]."},{"key":"14_CR118","first-page":"1121","volume":"33","author":"D. Wang","year":"1988","unstructured":"Wang, D.: Proving-by-examples method and inclusion of varieties. Kexue Tongbao 33: 1121\u20131123 (1988).","journal-title":"Kexue Tongbao"},{"key":"14_CR119","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1007\/BF01231031","volume":"36","author":"D. Wang","year":"1989","unstructured":"Wang, D.: A new theorem discovered by computer prover. J. Geom. 36: 173\u2013182 (1989).","journal-title":"J. Geom."},{"key":"14_CR120","unstructured":"Wang, D.: On Wu's method for proving constructive geometric theorems. In: Proc. IJCAI '89 (Detroit, August 20\u201325, 1989), pp. 419\u2013424."},{"key":"14_CR121","volume-title":"Medlar 24-month deliverables","author":"D. Wang","year":"1991","unstructured":"Wang, D.: Reasoning about geometric problems using algebraic methods. In: Medlar 24-month deliverables, DOC, Imperial College, Univ. of London, England (1991)."},{"key":"14_CR122","doi-asserted-by":"crossref","first-page":"471","DOI":"10.1016\/0167-8396(92)90045-Q","volume":"9","author":"D. Wang","year":"1992","unstructured":"Wang, D.: Irreducible decomposition of algebraic varieties via characteristic sets and Gr\u00f6bner bases. Comput. Aided Geom. Design 9: 471\u2013484 (1992).","journal-title":"Comput. Aided Geom. Design"},{"key":"14_CR123","volume-title":"Medlar II Report PPR1","author":"D. Wang","year":"1993","unstructured":"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\u201321, 1995), 561\u2013570."},{"key":"14_CR124","first-page":"386","volume":"814","author":"D. Wang","year":"1994","unstructured":"Wang, D.: Algebraic factoring and geometry theorem proving. In: LNCS 814, pp. 386\u2013400 (1994).","journal-title":"LNCS"},{"key":"14_CR125","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/978-3-7091-6604-8_8","volume-title":"Automated practical reasoning: Algebraic approaches","author":"D. Wang","year":"1995","unstructured":"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\u2013185 (1995)."},{"key":"14_CR126","series-title":"Ann. Math. Artif. Intell. 13(1,2)","first-page":"1","volume-title":"Algebraic approaches to geometric reasoning","author":"D. Wang","year":"1995","unstructured":"Wang, D.: Elimination procedures for mechanical theorem proving in geometry. In [66]: 1\u201324 (1995)."},{"key":"14_CR127","first-page":"658","volume":"1","author":"D. Wang","year":"1995","unstructured":"Wang, D.: A method for proving theorems in differential geometry and mechanics. J. Univ. Comput. Sci. 1: 658\u2013673 (1995).","journal-title":"J. Univ. Comput. Sci."},{"key":"14_CR128","doi-asserted-by":"crossref","unstructured":"Wang, D.: GEOTHER: A geometry theorem prover. In: Proc. CADE-13 (New Brunswick, July 30\u2013August 3, 1996), to appear.","DOI":"10.1007\/3-540-61511-3_78"},{"key":"14_CR129","first-page":"75","volume-title":"Mathematics-Mechanization Research Preprints, no. 2","author":"D. Wang","year":"1987","unstructured":"Wang, D., Gao, X.-S.: Geometry theorems proved mechanically using Wu's method \u2014 Part on Euclidean geometry. In [99]: 75\u2013106 (1987)."},{"key":"14_CR130","first-page":"163","volume":"7","author":"D. Wang","year":"1987","unstructured":"Wang, D., Hu, S.: A mechanical proving system for constructible theorems in elementary geometry. J. SSMS 7: 163\u2013172 (1987) [in Chinese].","journal-title":"J. SSMS"},{"key":"14_CR131","first-page":"356","volume":"358","author":"F. Winkler","year":"1988","unstructured":"Winkler, F.: A geometrical decision algorithm based on the Gr\u00f6bner bases algorithm. In: LNCS 358, pp. 356\u2013363 (1988).","journal-title":"LNCS"},{"key":"14_CR132","first-page":"15","volume":"1","author":"F. Winkler","year":"1990","unstructured":"Winkler, F.: Gr\u00f6bner bases in geometry theorem proving and simplest degeneracy conditions. Math. Pannonica 1: 15\u201332 (1990).","journal-title":"Math. Pannonica"},{"key":"14_CR133","first-page":"183","volume-title":"Issues in robotics and nonlinear geometry","author":"F. Winkler","year":"1992","unstructured":"Winkler, F.: Automated theorem proving in nonlinear geometry. In: Issues in robotics and nonlinear geometry (Hoffmann, C., ed.), JAI Press, Greenwich, pp. 183\u2013197 (1992)."},{"key":"14_CR134","volume-title":"Tech. Memo. 28","author":"R. Wong","year":"1972","unstructured":"Wong, R.: Construction heuristics for geometry and a vector algebra representation of geometry. Tech. Memo. 28, Project MAC, MIT, Cambridge, USA (1972)."},{"key":"14_CR135","first-page":"96","volume-title":"Mathematics-Mechanization Research Preprints, no. 7","author":"T.-J. Wu","year":"1991","unstructured":"Wu, T.-J.: On a collision problem. In [99]: 96\u2013104 (1991)."},{"key":"14_CR136","first-page":"159","volume":"21","author":"W. Wu","year":"1978","unstructured":"Wu, W.-t.: On the decision problem and the mechanization of theorem-proving in elementary geometry. Sci. Sinica 21: 159\u2013172 (1978). Also in [9], pp. 213\u2013234 (1984).","journal-title":"Sci. Sinica"},{"key":"14_CR137","first-page":"94","volume":"I","author":"W. Wu","year":"1979","unstructured":"Wu, W.-t.: On the mechanization of theorem-proving in elementary differential geometry. Sci. Sinica Special Issue on Math. (I): 94\u2013102 (1979) [in Chinese].","journal-title":"Sci. Sinica Special Issue on Math."},{"key":"14_CR138","unstructured":"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\u2013September 21, 1980), pp. 1073\u20131092."},{"key":"14_CR139","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1016\/S0252-9602(18)30628-3","volume":"2","author":"W. Wu","year":"1982","unstructured":"Wu, W.-t.: Toward mechanization of geometry \u2014 Some comments on Hilbert's \u201cGrundlagen der Geometrie\u201d. Acta Math. Scientia 2: 125\u2013138 (1982).","journal-title":"Acta Math. Scientia"},{"key":"14_CR140","doi-asserted-by":"crossref","first-page":"357","DOI":"10.1016\/S0252-9602(18)30616-7","volume":"3","author":"W. Wu","year":"1983","unstructured":"Wu, W.-t.: Some remarks on mechanical theorem-proving in elementary geometry. Acta Math. Scientia 3: 357\u2013360 (1983).","journal-title":"Acta Math. Scientia"},{"key":"14_CR141","first-page":"207","volume":"4","author":"W. Wu","year":"1984","unstructured":"Wu, W.-t.: Basic principles of mechanical theorem proving in elementary geometries. J. SSMS 4: 207\u2013235 (1984). Also in JAR 2: 221\u2013252 (1986).","journal-title":"J. SSMS"},{"key":"14_CR142","volume-title":"Basic principles of mechanical theorem proving in geometries (part on elementary geometries)","author":"W. Wu","year":"1984","unstructured":"Wu, W.-t.: Basic principles of mechanical theorem proving in geometries (part on elementary geometries). Science Press, Beijing (1984) [in Chinese]. English Translation, Springer, Wien-New York (1994)."},{"key":"14_CR143","series-title":"Comptemp. Math. 29","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1090\/conm\/029\/13","volume-title":"Automated theorem proving: After 25 years","author":"W. Wu","year":"1984","unstructured":"Wu, W.-t.: Some recent advances in mechanical theorem-proving of geometries. In [9], pp. 235\u2013241 (1984)."},{"key":"14_CR144","first-page":"1","volume":"1","author":"W. Wu","year":"1986","unstructured":"Wu, W.-t.: A mechanization method of geometry I. Chinese Quart. J. Math. 1: 1\u201314 (1986).","journal-title":"Chinese Quart. J. Math."},{"key":"14_CR145","first-page":"204","volume":"6","author":"W. Wu","year":"1986","unstructured":"Wu, W.-t.: A mechanization method of geometry and its applications I. J. SSMS 6: 204\u2013216 (1986).","journal-title":"J. SSMS"},{"key":"14_CR146","first-page":"175","volume":"1","author":"W. Wu","year":"1986","unstructured":"Wu, W.-t.: A report on mechanical theorem proving and mechanical theorem discovering in geometries. Adv. Sci. China Math. 1: 175\u2013198 (1986).","journal-title":"Adv. Sci. China Math."},{"key":"14_CR147","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1007\/BFb0077689","volume":"1255","author":"W. Wu","year":"1987","unstructured":"Wu, W.-t.: A constructive theory of differential algebraic geometry. In: Lecture Notes in Math. 1255, pp. 173\u2013189 (1987).","journal-title":"Lecture Notes in Math."},{"key":"14_CR148","first-page":"585","volume":"32","author":"W. Wu","year":"1987","unstructured":"Wu, W.-t.: A mechanization method of geometry and its applications II. Kexue Tongbao 32: 585\u2013588 (1987).","journal-title":"Kexue Tongbao"},{"key":"14_CR149","first-page":"1","volume":"2","author":"W. Wu","year":"1987","unstructured":"Wu, W.-t.: On reducibility problem in mechanical theorem proving of elementary geometries. Chinese Quart. J. Math. 2: 1\u201320 (1987).","journal-title":"Chinese Quart. J. Math."},{"key":"14_CR150","first-page":"1","volume":"1","author":"W. Wu","year":"1988","unstructured":"Wu, W.-t.: A mechanization method of geometry and its applications III. SSMS 1: 1\u201317 (1988).","journal-title":"SSMS"},{"key":"14_CR151","first-page":"97","volume":"2","author":"W. Wu","year":"1989","unstructured":"Wu, W.-t.: A mechanization method of geometry and its applications IV. SSMS 2: 97\u2013109 (1989).","journal-title":"SSMS"},{"key":"14_CR152","unstructured":"Wu, W.-t.: Equations-solving and theorems-proving \u2014 Zero-set formulation and ideal formulation. In: Proc. Asian Math. Conf. (Hong Kong, August 14\u201318, 1990), pp. 1\u201310."},{"key":"14_CR153","first-page":"171","volume":"7","author":"W. Wu","year":"1991","unstructured":"Wu, W.-t.: Mechanical theorem proving of differential geometries and some of its applications in mechanics. JAR 7: 171\u2013191 (1991).","journal-title":"JAR"},{"key":"14_CR154","first-page":"1","volume":"2","author":"W. Wu","year":"1992","unstructured":"Wu, W.-t.: A report on mechanical geometry theorem proving. Progr. Natur. Sci. 2: 1\u201317 (1992).","journal-title":"Progr. Natur. Sci."},{"key":"14_CR155","first-page":"103","volume-title":"Issues in robotics and nonlinear geometry","author":"W. Wu","year":"1992","unstructured":"Wu, W.-t.: A mechanization method of equations solving and theorem proving. In: Issues in robotics and nonlinear geometry (Hoffmann, C., ed.), JAI Press, Greenwich, pp. 103\u2013138 (1992)."},{"key":"14_CR156","first-page":"1","volume-title":"Mathematics-Mechanization Research Preprints, no. 7","author":"W. Wu","year":"1992","unstructured":"Wu, W.-t.: On problems involving inequalities. In [99]: 1\u201313 (1992)."},{"key":"14_CR157","first-page":"193","volume":"7","author":"W. Wu","year":"1994","unstructured":"Wu, W.-t.: On a finiteness theorem about problems involving inequalities. SSMS 7: 193\u2013200 (1994).","journal-title":"SSMS"},{"key":"14_CR158","first-page":"1","volume-title":"Mathematics-Mechanization Research Preprints, no. 13","author":"W. Wu","year":"1995","unstructured":"Wu, W.-t.: Central configurations in planet motions and vortex motions. In [99]: 1\u201314 (1995)."},{"key":"14_CR159","volume-title":"Triangles with equal bisectors","author":"W. Wu","year":"1985","unstructured":"Wu, W.-t., L\u00fc, X.-L.: Triangles with equal bisectors. People's Edu. Press, Beijing (1985) [in Chinese]."},{"key":"14_CR160","first-page":"26","volume":"no. 3","author":"W. Wu","year":"1994","unstructured":"Wu, W.-t., Wang, D.-K.: The algebraic surface fitting problem in CAGD. Math. Practice Theory no. 3: 26\u201331 (1994) [in Chinese].","journal-title":"Math. Practice Theory"},{"key":"14_CR161","unstructured":"Xu, C., Shi, Q., Cheng, M.: A global stereo vision method based on Wu-solver. In: Proc. GMICV '95 (Xi'an, April 27\u201329, 1995), pp. 198\u2013205."},{"key":"14_CR162","unstructured":"Xu, L., Chen, J.: AUTOBASE: A system which automatically establishes the geometry knowledge base. In: Proc. COMPINT: Computer aided technologies (Montreal, September 8\u201312, 1985), pp. 708\u2013714."},{"key":"14_CR163","unstructured":"Xu, L., Chen, J., Yang, L.: Solving plane geometry problem by learning. In: Proc. IEEE 1st Int. Conf. Comput. Appl. (Beijing, June 20\u201322, 1984), pp. 862\u2013869."},{"key":"14_CR164","first-page":"115","volume-title":"The mathematical revolution inspired by computing","author":"L. Yang","year":"1991","unstructured":"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\u2013126 (1991)."},{"key":"14_CR165","first-page":"147","volume-title":"Artificial intelligence in mathematics","author":"L. Yang","year":"1994","unstructured":"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\u2013156 (1994)."},{"key":"14_CR166","first-page":"547","volume":"37","author":"L. Yang","year":"1994","unstructured":"Yang, L., Zhang, J.-Z., Hou, X.-R.: A criterion for dependency of algebraic equations, with applications to automated theorem proving. Sci. China Ser. A 37: 547\u2013554 (1994).","journal-title":"Sci. China Ser. A"},{"key":"14_CR167","unstructured":"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\u201320, 1995), pp. 33\u201341."},{"key":"14_CR168","unstructured":"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\u201318, 1992), pp. 244\u2013250."},{"key":"14_CR169","volume-title":"How to solve geometry problems using areas","author":"J.-Z. Zhang","year":"1982","unstructured":"Zhang, J.-Z.: How to solve geometry problems using areas. Shanghai Edu. Publ., Shanghai (1982) [in Chinese]."},{"key":"14_CR170","series-title":"Ann. Math. Artif. Intell. 13(1,2)","first-page":"109","volume-title":"Algebraic approaches to geometric reasoning","author":"J.-Z. Zhang","year":"1995","unstructured":"Zhang, J.-Z., Chou, S.-C., Gao, X.-S.: Automated production of traditional proofs for theorems in Euclidean geometry I. In [66]: 109\u2013137 (1995)."},{"key":"14_CR171","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1016\/0304-3975(90)90077-U","volume":"74","author":"J.-Z. Zhang","year":"1990","unstructured":"Zhang, J.-Z., Yang, L., Deng, M.-K.: The parallel numerical method of mechanical theorem proving. Theoret. Comput. Sci. 74: 253\u2013271 (1990).","journal-title":"Theoret. Comput. Sci."}],"container-title":["Lecture Notes in Computer Science","Artificial Intelligence and Symbolic Mathematical Computation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61732-9_60.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T23:25:18Z","timestamp":1742599518000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61732-9_60"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540617327","9783540707400"],"references-count":171,"URL":"https:\/\/doi.org\/10.1007\/3-540-61732-9_60","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1996]]}}}