{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,3]],"date-time":"2026-02-03T16:12:11Z","timestamp":1770135131318,"version":"3.49.0"},"reference-count":170,"publisher":"Elsevier","isbn-type":[{"value":"9780444508133","type":"print"}],"license":[{"start":{"date-parts":[[2001,1,1]],"date-time":"2001-01-01T00:00:00Z","timestamp":978307200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1016\/b978-044450813-3\/50013-8","type":"book-chapter","created":{"date-parts":[[2007,6,11]],"date-time":"2007-06-11T13:04:11Z","timestamp":1181567051000},"page":"707-749","source":"Crossref","is-referenced-by-count":23,"title":["Automated Reasoning in Geometry"],"prefix":"10.1016","author":[{"given":"Shang-Ching","family":"Chou","sequence":"first","affiliation":[]},{"given":"Xiao-Shan","family":"Gao","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/B978-044450813-3\/50013-8_bb0010","series-title":"Proc. IJCAI'81","first-page":"165","article-title":"Turning the search of the problem space for geometry proofs","author":"Anderson","year":"1981"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0015","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1016\/0004-3702(88)90049-5","article-title":"Geometric reasoning with logic and algebra","volume":"37","author":"Arnon","year":"1988","journal-title":"Artificial Intelligence"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0020","doi-asserted-by":"crossref","first-page":"237","DOI":"10.1016\/S0747-7171(88)80014-2","article-title":"On mechanical quantifier elimination for elementary algebra and geometry","volume":"5","author":"Arnon","year":"1988","journal-title":"J. of Symbolic Computation"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0025","series-title":"Lncs 968","first-page":"31","article-title":"Equation solving in geometrical theories","author":"Balbiani","year":"1995"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0030","series-title":"Lncs 909","first-page":"196","article-title":"Affine geometry of collinearity and conditional term rewriting","author":"Balbiani","year":"1995"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0035","series-title":"Adg'98, LNAI 1669","first-page":"207","article-title":"An application of automatic theorem proving in computer vision","author":"Bondyfalat","year":"1999"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0040","series-title":"Adg'98, LNAI 1669","first-page":"130","article-title":"Clifford term rewriting for geometric reasoning in 3d","author":"Boy de la Tour","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0045","doi-asserted-by":"crossref","first-page":"894","DOI":"10.1090\/S0002-9904-1948-09091-7","article-title":"A note on Hilbert's nullstellensatz","volume":"54","author":"Brauer","year":"1948","journal-title":"Bull. Amer. Math. Soc."},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0050","series-title":"Proc. of Workshop on Interactive 3D Graphics","first-page":"111","article-title":"Constructing three-dimensional geometric objects defined by constraints","author":"Br\u00fcderlin","year":"1986"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0055","series-title":"Multidimensional Systems Theory","first-page":"184","article-title":"Gr\u00f6bner bases: An algorithmic method in polynomial ideal theory","author":"Buchberger","year":"1985"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0060","first-page":"85","article-title":"Algebraic methods for geometric reasoning","volume":"19","author":"Buchberger","year":"1995","journal-title":"Ann. Rev. Comput. Sci."},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0065","series-title":"Les Syst\u00e8mes Diff\u00e9rentiels Ext\u00e9rieurs et leurs Applications G\u00e9ometriques","author":"Cartan","year":"1946"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0070","series-title":"Automated Theorem Proving: After 25 years","first-page":"243","article-title":"Proving elementary geometry theorems using Wu's algorithm","author":"Chou","year":"1984"},{"key":"10.1016\/B978-044450813-3\/50013-8_rf0075","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1007\/BF00243793","article-title":"A method for mechanical derivation of formulae in elementary geometry","volume":"3","author":"Chou","year":"1987","journal-title":"J. of Automated Reasoning"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0080","series-title":"Mechanical Geometry Theorem Proving","author":"Chou","year":"1988"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0085","series-title":"Proc. of ISSAC'90","first-page":"255","article-title":"Automated reasoning in geometry using the CS and GB methods","author":"Chou","year":"1990"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0090","article-title":"A collection of 120 computer solved geometry problems in mechanical formula derivation","author":"Chou","year":"1989","journal-title":"Technical Report TR-89-22, CS Department, The Univ. of Texas at Austin"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0095","series-title":"Proc. of ISSAC'90 (Tokyo)","first-page":"265","article-title":"Mechanical formula derivation in elementary geometries","author":"Chou","year":"1990"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0100","series-title":"Proc. of CADE-10","first-page":"207","article-title":"Ritt-Wu's decomposition algorithm and geometry theorem proving","author":"Chou","year":"1990"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0105","article-title":"Geometry theorems proved mechanically using Wu's method, part on differential geometry","author":"Chou","year":"1991","journal-title":"Technical Report MM Preprints, NO. 6, MMRC, Academia Sinica"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0110","series-title":"Proc. of CADE-11","first-page":"20","article-title":"Proving geometry statements of constructive type","author":"Chou","year":"1992"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0115","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1007\/BF00881834","article-title":"Automated reasoning in differential geometry and mechanics: Part i. an improved version of Ritt-Wu's decomposition algorithm","volume":"10","author":"Chou","year":"1993","journal-title":"J. of Automated Reasoning"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0120","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1007\/BF00881835","article-title":"Automated reasoning in differential geometry and mechanics: Part ii. mechanical theorem proving","volume":"10","author":"Chou","year":"1993","journal-title":"J. of Automated Reasoning"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0125","first-page":"1","article-title":"Automated reasoning in differential geometry and mechanics: Part iii. mechanical formula derivation","author":"Chou","year":"1993","journal-title":"Ifip Tran. on Automated Reasoning"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0130","first-page":"186","article-title":"Automated reasoning in differential geometry and mechanics: Part iv. Bertrand curves","volume":"6","author":"Chou","year":"1993","journal-title":"J. of Sys. Sci. and Math. Sci."},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0135","series-title":"Computer Mathematics","first-page":"136","article-title":"Mechanical theorem proving in Riemannian geometry using Wu's method","author":"Chou","year":"1993"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0140","first-page":"139","article-title":"On the mechanical proof of geometry theorems involving inequalities","volume":"6","author":"Chou","year":"1992","journal-title":"Advances in Computing Research"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0145","article-title":"A combination of Ritt-Wu's method and Collins' method","author":"Chou","year":"1989","journal-title":"Technical Report TR-89-28, CS Department, The Univ. of Texas at Austin"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0150","series-title":"Proc. of Eighth IEEE Symposium on Logic in Computer Science","first-page":"48","article-title":"Automated production of traditional proofs for constructive geometry theorems","author":"Chou","year":"1993"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0155","series-title":"Proc. of ISSAC'93 (Kiev)","first-page":"284","article-title":"Mechanical geometry theorem proving by vector calculation","author":"Chou","year":"1993"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0160","series-title":"Machine Proofs in Geometry \u2013 Automated Production of Readable Proofs for Geometry Theorems","author":"Chou","year":"1994"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0165","doi-asserted-by":"crossref","first-page":"257","DOI":"10.1007\/BF00881858","article-title":"Automated production of traditional proofs in solid geometry","volume":"14","author":"Chou","year":"1995","journal-title":"J. of Automated Reasoning"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0170","doi-asserted-by":"crossref","first-page":"325","DOI":"10.1007\/BF00283133","article-title":"Automated generation of readable proofs with geometric invariants part i: Multiple and shortest proof generation","volume":"17","author":"Chou","year":"1996","journal-title":"J. of Automated Reasoning"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0175","doi-asserted-by":"crossref","first-page":"349","DOI":"10.1007\/BF00283134","article-title":"Automated generation of readable proofs with geometric invariants part ii: Theorem proving with full angles","volume":"17","author":"Chou","year":"1996","journal-title":"J. of Automated Reasoning"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0180","article-title":"A deductive database approach to automated geometry theorem proving and discovering","author":"Chou","year":"1996","journal-title":"accepted by Journal of Automated Reasoning"},{"key":"10.1016\/B978-044450813-3\/50013-8_rf0185","series-title":"Proc. of IEEE Symp. of Logic in Computer Science","first-page":"187","article-title":"On mechanical theorem proving in Minkowskian plane geometry","author":"Chou","year":"1986"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0190","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1007\/BF02328448","article-title":"Proving geometry theorems with rewrite rules","volume":"2","author":"Chou","year":"1986","journal-title":"J. of Automated Reasoning"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0195","doi-asserted-by":"crossref","first-page":"237","DOI":"10.1007\/BF01553889","article-title":"On the algebraic formulation of certain geometry statements and mechanical geometry theorem proving","volume":"4","author":"Chou","year":"1989","journal-title":"Algorithmica"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0200","doi-asserted-by":"crossref","first-page":"329","DOI":"10.1007\/BF00248249","article-title":"Automated reasoning in geometry theorem proving with Prolog","volume":"2","author":"Coelho","year":"1986","journal-title":"J. of Automated Reasoning"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0205","first-page":"134","article-title":"Quantifier elimination for real closed fields by cylindrical algebraic decomposition","author":"Collins","year":"1975"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0210","doi-asserted-by":"crossref","first-page":"299","DOI":"10.1016\/S0747-7171(08)80152-6","article-title":"Partial CAD construction in quantifier elimination","author":"Collins","year":"1991","journal-title":"J. of Symbolic Computation"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0215","first-page":"183","article-title":"A case of automatic theorem proving in Euclidean geometry","author":"Conti","year":"1995"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0220","doi-asserted-by":"crossref","first-page":"204","DOI":"10.2307\/2975007","article-title":"The rise, fall and possible transfiguration of triangle geometry","volume":"102","author":"Davis","year":"1995","journal-title":"The American Mathematical Monthly"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0225","doi-asserted-by":"crossref","first-page":"895","DOI":"10.2307\/2317942","article-title":"Formac meets Pappus","volume":"76","author":"Davis","year":"1969","journal-title":"The American Mathematical Monthly"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0230","series-title":"Adg'98","first-page":"14","article-title":"Solving geometric problems with real quantifier elimination","author":"Dolzmann","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0235","article-title":"A new approach for automatic theorem proving in real geometry","author":"Dolzmann","year":"1996","journal-title":"Technical Report TR MIP-9611, to appear in JAR, Universit\u00e4t Passau"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0240","series-title":"Computer Aided Geometric Reasoning, Proc. INRIA Workshop, Rocquencourt","year":"1987"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0245","series-title":"Adg'98, LNAI 1669","first-page":"86","article-title":"Plane Euclidean reasoning","author":"Fearnley-Sander","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0250","series-title":"Lnai 1360","first-page":"141","article-title":"Area in Grassmann geometry","author":"Fearnley-Sander","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0255","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1007\/BF00245819","article-title":"A procedure to prove statements in differential geometry","volume":"6","author":"Ferro","year":"1990","journal-title":"J. Automated Reasoning"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0260","doi-asserted-by":"crossref","first-page":"351","DOI":"10.1007\/BF00885765","article-title":"An extension of a procedure to prove statements in differential geometry","volume":"12","author":"Ferro","year":"1994","journal-title":"J. Automated Reasoning"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0265","series-title":"Lnai 1360","first-page":"87","article-title":"Probabilistic verification of elementary geometry statements","author":"Ferro","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0270","series-title":"Adg'96, LNAI 1360","first-page":"218","article-title":"Integration of reasoning and algebraic calculus in geometry","author":"F\u00e8vre","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0275","series-title":"Lnai 1421","first-page":"17","article-title":"Proving geometric theorems using Clifford algebra and rewrite rules","author":"F\u00e8vre","year":"1997"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0280","series-title":"Proc. AISC'98","first-page":"145","article-title":"Combining algebraic computing and term-rewriting for geometry theorem proving","author":"F\u00e8vre","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0285","series-title":"Adg'98, LNAI 1669","first-page":"47","article-title":"Proving Newton's propositio Kepleriana using geometry and nonstandard analysis in Isabelle","author":"Fleuriot","year":"1998"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50013-8_bb0290","doi-asserted-by":"crossref","first-page":"153","DOI":"10.1145\/356924.356929","article-title":"Logic and databases: A deductive approach","volume":"16","author":"Gallaire","year":"1984","journal-title":"ACM Computing Surveys"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0295","doi-asserted-by":"crossref","first-page":"403","DOI":"10.1007\/BF00244356","article-title":"Transcendental functions and mechanical theorem proving in elementary geometries","volume":"6","author":"Gao","year":"1990","journal-title":"J. of Automated Reasoning"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0300","series-title":"Proc. of ASCM'98","first-page":"185","article-title":"On the solution classification of the \u201cP3P\u201d problem","author":"Gao","year":"1998"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50013-8_bb0305","doi-asserted-by":"crossref","first-page":"47","DOI":"10.1016\/S0010-4485(97)00052-3","article-title":"Solving geometric constraint systems, i. a global propagation approach","volume":"30","author":"Gao","year":"1998","journal-title":"Computer Aideded Design"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50013-8_rf0310","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1016\/S0010-4485(97)00055-9","article-title":"Solving geometric constraint systems, ii. a symbolic computational approach","volume":"30","author":"Gao","year":"1998","journal-title":"Computer Aideded Design"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0315","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1007\/BF01224042","article-title":"On the automatic derivation of a set of geometric formulae","volume":"53","author":"Gao","year":"1995","journal-title":"J. of Geometry"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0320","series-title":"Geometry Expert","author":"Gao","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0325","series-title":"Proc. of ASCM'98","first-page":"15","article-title":"Building dynamic mathematical models with geometry expert, ii. linkages","author":"Gao","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0330","series-title":"Proc. of ATCM'98, (Tsukuba Japan)","first-page":"216","article-title":"Building dynamic mathematical models with geometry expert, i. geometric transformations, functions and plane curves","author":"Gao","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0335","series-title":"Proc. Int. Conf. in Info. Process","first-page":"273","article-title":"Realization of a geometry theorem machine","author":"Gelernter","year":"1959"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0340","series-title":"Proc. West. Joint Computer Conf.","first-page":"143","article-title":"Empirical explorations of the geometry-theorem proving machine","author":"Gelernter","year":"1960"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0345","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1016\/S0747-7171(88)80040-3","article-title":"Gr\u00f6bner bases and primary decomposition of polynomial ideals","volume":"6","author":"Gianni","year":"1988","journal-title":"J. of Symbolic Computation"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0350","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1016\/0004-3702(70)90005-6","article-title":"An examination of the geometry theorem machine","volume":"1","author":"Gilmore","year":"1970","journal-title":"Artificial Intelligence"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0355","series-title":"Proc. ISSAC'94 (Oxford)","first-page":"20","article-title":"Examples of automatic theorem proving in real geometry","author":"Guergueb","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0360","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1016\/S0747-7171(08)80120-4","article-title":"Some examples of the use of distances as coordinates for Euclidean geometry","volume":"11","author":"Havel","year":"1991","journal-title":"J. of Symbolic Computation"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0365","series-title":"Automated Deduction in Geometry","first-page":"102","article-title":"Computational synthetic geometry with Clifford algebraic","author":"Havel","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0370","series-title":"Foundations of Geometry","author":"Hilbert","year":"1971"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0375","series-title":"Computing in Euclidean Geometry","first-page":"266","article-title":"Geometric constraint solving in R2 and R3","author":"Hoffmann","year":"1995"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0380","doi-asserted-by":"crossref","first-page":"195","DOI":"10.1007\/BF01531329","article-title":"Short description of existing provers","volume":"13","author":"Hong","year":"1995","journal-title":"Ann. Math. Artif. Intell"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0385","first-page":"824","article-title":"Can geometry be proved by an example?","volume":"29","author":"Hong","year":"1986","journal-title":"Scientia Sinica"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0390","series-title":"Proc. IWMM'92","first-page":"181","article-title":"Kinematic solution of a Stewart platform","author":"Huang","year":"1992"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0395","first-page":"73","article-title":"A generalized Euclidean algorithm for geometry theorem proving","volume":"13","author":"Kalkbrener","year":"1995","journal-title":"Ann. of Math. and AI"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0400","series-title":"Proc. of SYMSAC'86, (Toronto)","first-page":"202","article-title":"Geometry theorem proving using Hilbert's nullstellensatz","author":"Kapur","year":"1986"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0405","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1016\/0004-3702(88)90050-1","article-title":"A refutational approach to geometry theorem proving","volume":"37","author":"Kapur","year":"1988","journal-title":"Artificial Intelligence"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0410","series-title":"Automated Deduction in Geometry","first-page":"1","article-title":"Automated geometric reasoning: Dixon resultants, Gr\u00f6bner bases and characteristic sets","author":"Kapur","year":"1997"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0415","doi-asserted-by":"crossref","first-page":"15","DOI":"10.1016\/0004-3702(88)90048-3","article-title":"Wu's method and its application to perspective viewing","volume":"37","author":"Kapur","year":"1988","journal-title":"Artificial Intelligence"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0420","series-title":"Invited Talk, IMACS-95","article-title":"Automated geometry theorem proving using the Dixon resultants","author":"Kapur","year":"1995"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0425","series-title":"Proc. of ISSAC'94, (Oxford)","first-page":"99","article-title":"Algebraic and geometric reasoning with Dixon resultants","author":"Kapur","year":"1994"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0430","series-title":"Proc. of ISSAC'90, (Tokyo)","first-page":"277","article-title":"Refutational proofs of geometry theorems via characteristic set computation","author":"Kapur","year":"1990"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0435","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1016\/0004-3702(88)90051-3","article-title":"Geometry theorem proving by decomposition of quasi-algebraic sets: An application of the Ritt-Wu principle","volume":"37","author":"Ko","year":"1988","journal-title":"Artificial Intelligence"},{"key":"10.1016\/B978-044450813-3\/50013-8_rf0440","article-title":"Alge-prover \u2013 an algebraic geometry theorem proving software","author":"Ko","year":"1985","journal-title":"Technical Report Technical Report, 85CRD139, General Electric Company"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0445","doi-asserted-by":"crossref","first-page":"511","DOI":"10.1207\/s15516709cog1404_2","article-title":"Abstract planning and perceptual chunks: Elements of expertise in geometry","volume":"14","author":"Koedinger","year":"1990","journal-title":"Cognitive Science"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0450","series-title":"Solving Geometric Constraint Systems","author":"Kramer","year":"1992"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0455","series-title":"Proc. of ISSACC'89","first-page":"254","article-title":"Careful algebraic translations of geometry theorems","author":"Kutzler","year":"1989"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0460","series-title":"Proc. of SYMSAC'86, (Toronto)","first-page":"209","article-title":"Automated geometry theorem proving using Buchberger's algorithm","author":"Kutzler","year":"1986"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0465","series-title":"Adg'98, LNAI 1669","first-page":"67","article-title":"Readable machine solving in geometry and icai software msg","author":"Li","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0470","series-title":"Proc. ASCM'95 (Beijing)","first-page":"29","article-title":"Automated reasoning with differential forms","author":"Li","year":"1995"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0475","series-title":"Adg'98, LNAI 1669","first-page":"156","article-title":"Some applications of Clifford algebra to geometries","author":"Li","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0480","series-title":"J. Automated Reasoning (accepted)","article-title":"Vectorial equations solving for mechanical geometry theorem proving","author":"Li","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0485","article-title":"Proving geometric theorems with Clifford algebraic method","author":"Li","year":"1996","journal-title":"Technical Report MM Preprints, NO. 14, MMRC, Academia Sinica"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0490","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1023\/A:1005819428156","article-title":"Proving geometric theorems with Clifford in differential geometries","volume":"21","author":"Li","year":"1998","journal-title":"J. Automated Reasoning"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50013-8_bb0495","doi-asserted-by":"crossref","first-page":"221","DOI":"10.1007\/BF02559961","article-title":"On erdos' ten-point problem","volume":"13","author":"Li","year":"1997","journal-title":"Acta Mathematica Sinica, New Series"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0500","first-page":"25","article-title":"Mechanical theorem-proving of the local theory of the surfaces","volume":"13","author":"Li","year":"1995","journal-title":"Ann. of Math. and AI"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0505","series-title":"Proc. IWMM'92","first-page":"222","article-title":"Some results on theorem proving in finite geometry","author":"Lin","year":"1992"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0510","doi-asserted-by":"crossref","first-page":"773","DOI":"10.1109\/TC.1976.1674696","article-title":"Problems and experiments for and with automated theorem-proving programs","volume":"C-25","author":"McCharen","year":"1976","journal-title":"IEEE Trans. on Computers"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0515","series-title":"Proc. CADE-12","first-page":"401","article-title":"A combination of Ritt-Wu's method and Collins' method","author":"McPhee","year":"1994"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0520","series-title":"Recent Advances in Geometric Inequalities","author":"Mitrinovic","year":"1989"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0525","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0004-3702(75)90013-2","article-title":"Plane geometry theorem proving using forward chaining","volume":"6","author":"Nevins","year":"1976","journal-title":"Artificial Intelligence"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0530","series-title":"Proc. ACM Symp. Found. of Solid Modeling, (Austin TX)","first-page":"397","article-title":"Algebraic solution for geometry from dimensional constraints","author":"Owen","year":"1991"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0535","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1007\/BF00245024","article-title":"Automated development of Tarski geometry","volume":"5","author":"Quaife","year":"1989","journal-title":"J. of Automated Reasoning"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0540","series-title":"Proc. 11th Ann. Symp. Comp. Geom.","first-page":"277","article-title":"A complete and practical algorithm for geometric proving","author":"Rege","year":"1995"},{"issue":"4","key":"10.1016\/B978-044450813-3\/50013-8_bb0545","doi-asserted-by":"crossref","first-page":"328","DOI":"10.1109\/TC.1976.1674613","article-title":"A semantically guided deductive system for automatic theorem proving","volume":"C-25","author":"Reiter","year":"1977","journal-title":"IEEE Tras. on Computers"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0550","first-page":"139","article-title":"Mechanical theorem proving in projective geometry","volume":"13","author":"Richter-Gebert","year":"1995","journal-title":"Ann. of Math. and AI"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0555","series-title":"Cinderella","author":"Richter-Gebert","year":"1999"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0560","series-title":"Differential Equation from Algebraic Standpoint, Vol. 14","author":"Ritt","year":"1938"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0565","series-title":"Differential Algebra","author":"Ritt","year":"1950"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0570","series-title":"Automation of Reasoning","first-page":"74","article-title":"Proving a theorem (as done by man, logician, or machine)","author":"Robinson","year":"1954"},{"key":"10.1016\/B978-044450813-3\/50013-8_rf0575","doi-asserted-by":"crossref","first-page":"365","DOI":"10.2307\/1969640","article-title":"A new decision method for elementary algebra","volume":"60","author":"Seidenberg","year":"1954","journal-title":"Annals of Math."},{"issue":"2","key":"10.1016\/B978-044450813-3\/50013-8_bb0580","first-page":"31","article-title":"An elimination theory for differential algebra","volume":"3","author":"Seidenberg","year":"1955","journal-title":"University of California Pub. in Math., New Series"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0585","series-title":"Proc. of ISSAC'93, (Kiev)","first-page":"301","article-title":"Geometry theorem proving in vector spaces by means of Gr\u00f6bner bases","author":"Stifter","year":"1993"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0590","article-title":"On the Algebraic and Algorithmic Properties of Some Generalized Algebras","author":"Stokes","year":"1990","journal-title":"PhD thesis, University of Tasmania"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0595","article-title":"A decision method for elementary algebra and geometry","author":"Tarski","year":"1951","journal-title":"Technical Report Report R-109, The Rand Corporation, Santa Monica"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0600","series-title":"Differential Systems","author":"Thomas","year":"1954"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0605","first-page":"1121","article-title":"Proving-by-examples method and inclusion of varieties","volume":"33","author":"Wang","year":"1988","journal-title":"Kexue Tongbao"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0610","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1007\/BF01231031","article-title":"A new theorem discovered by computer prover","volume":"36","author":"Wang","year":"1989","journal-title":"J. of Geometry"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0615","article-title":"Reasoning about geometric problems using an elimination method","author":"Wang","year":"1991","journal-title":"Technical Report Medlar 24-month deliverables, DOC, Imperial College, Univ. of London"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0620","series-title":"Proc. of IWMM'92","first-page":"236","article-title":"Mechanical solution of a group of space geometry problems","author":"Wang","year":"1992"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0625","article-title":"Polynomial Equations Solving and Mechanical Geometric Theorem Proving","author":"Wang","year":"1993","journal-title":"PhD thesis, Inst. of Sys. Sci., Academia Sinica, Beijing"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0630","first-page":"1","article-title":"Elimination procedures for mechanical theorem proving in geometry","volume":"13","author":"Wang","year":"1995","journal-title":"Ann. of Math. and AI"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0635","first-page":"658","article-title":"A method for proving theorems in differential geometry and mechanics","volume":"1","author":"Wang","year":"1995","journal-title":"J. Univ. Comput. Sci."},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0640","series-title":"Automated practical reasoning: Algebraic approaches","article-title":"Reasoning about geometric problems using an elimination method","author":"Wang","year":"1995"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0645","series-title":"Lnai 814","article-title":"Algebraic factoring and geometry theorem proving","author":"Wang","year":"1996"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0650","series-title":"Proc. AISMC-3, LNCS 1138","first-page":"213","article-title":"Geometry machines: From AI to SMC","author":"Wang","year":"1996"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0655","series-title":"Proc. of CADE-13, (New Brunswick)","article-title":"Geother: A geometry theorem prover","author":"Wang","year":"1996"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0660","series-title":"Adg'96, LNAI 1360","article-title":"Clifford algebraic calculus for geometric reasoning with application to computer vision","author":"Wang","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0665","series-title":"Gr\u00f6bner bases and applications","article-title":"Gr\u00f6bner bases applied to geometric theorem proving and discovering","author":"Wang","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0670","article-title":"Geometry theorems proved mechanically using Wu's method, part on elementary geometries","author":"Wang","year":"1987","journal-title":"Technical Report MM Research Preprint, No. 2, MMRC, Academia Sinica"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0675","first-page":"163","article-title":"Mechanical proving system for constructible theorems in elementary geometry","volume":"7","author":"Wang","year":"1987","journal-title":"J. Sys. Sci. and Math. Scis."},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0680","series-title":"Proc. ASCM'98","first-page":"23","article-title":"Algebraic factorization applied to geometric problems","author":"Wang","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0685","series-title":"Automated Deduction in Geometry","first-page":"386","article-title":"Computational geometry problems in REDLOG","author":"Weispfenning","year":"1994"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0690","series-title":"Proc. of ISSAC'88","first-page":"4","article-title":"Cayley factorization","author":"White","year":"1988"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0695","first-page":"15","article-title":"Gr\u00f6bner bases in geometry theorem proving and simplest degeneracy conditions","volume":"1","author":"Winkler","year":"1990","journal-title":"Math. Pannonica"},{"key":"10.1016\/B978-044450813-3\/50013-8_rf0700","first-page":"183","article-title":"Automated theorem proving in nonlinear geometry","volume":"6","author":"Winkler","year":"1992","journal-title":"Issues in Robotics and Nonlinear Geometry"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0705","doi-asserted-by":"crossref","first-page":"32","DOI":"10.1016\/S0252-9602(17)30761-0","article-title":"On a collision problem","volume":"15","author":"Wu","year":"1995","journal-title":"Acta Math. Scientia"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0710","first-page":"157","article-title":"On the decision problem and the mechanization of theorem proving in elementary geometry","volume":"21","author":"Wu","year":"1978","journal-title":"J. Sys. Sci. and Math. Scis."},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0715","first-page":"94","article-title":"Mechanical theorem proving in elementary differential geometry","author":"Wu","year":"1979","journal-title":"Scientia Sinica"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0720","series-title":"Proc. 1980 Beijing Symposium on Differential Geometry and Differential Equations","first-page":"125","article-title":"Mechanical theorem proving in elementary geometry and differential geometry","author":"Wu","year":"1982"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0725","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1016\/S0252-9602(18)30628-3","article-title":"Toward mechanization of geometry \u2013 some comments on Hilbert's Grundlagen der Geometrie","author":"Wu","year":"1982","journal-title":"Acta Math. Sci."},{"issue":"3","key":"10.1016\/B978-044450813-3\/50013-8_bb0730","first-page":"207","article-title":"Basic principles of mechanical theorem proving in geometries","volume":"4","author":"Wu","year":"1984","journal-title":"J. Sys. Sci. and Math. Scis."},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0735","series-title":"Basic Principles of Mechanical Theorem Proving in Geometries","author":"Wu","year":"1984"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0740","series-title":"Automated Theorem Proving: After 25 years","first-page":"235","article-title":"Some recent advances in mechanical theorem-proving of geometries","author":"Wu","year":"1984"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0745","first-page":"204","article-title":"A mechanization method of geometry and its applications i: Distances, areas, and volumes","volume":"6","author":"Wu","year":"1986","journal-title":"J. Sys. Sci. and Math. Scis."},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0750","first-page":"1","article-title":"On reducibility problem in mechanical theorem proving of elementary geometries","author":"Wu","year":"1986","journal-title":"Chinese Quart. J. Math."},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0755","first-page":"173","article-title":"A constructive theory of differential algebraic geometry","volume":"Vol. 1255","author":"Wu","year":"1987"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0760","article-title":"Mechanical derivation of Newton's gravitational laws from Kepler's law","author":"Wu","year":"1987","journal-title":"Technical Report MM Research Preprints No. 1, MMRC, Academia Sinica"},{"issue":"9","key":"10.1016\/B978-044450813-3\/50013-8_bb0765","first-page":"535","article-title":"A mechanization method of geometry and its applications ii: Curve pairs of Bertrand type","volume":"32","author":"Wu","year":"1987","journal-title":"Kexue Tongbao"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0770","first-page":"97","article-title":"A mechanization method of geometry and its applications iv. some theorems in planar kinematics","volume":"2","author":"Wu","year":"1989","journal-title":"J. Sys. Scis and Math. Sci."},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0775","article-title":"A mechanization method of geometry and its applications vi. solving inverse kinematics equations of PUMA-type robotics","author":"Wu","year":"1989","journal-title":"Technical Report MM Research Preprints No. 4, MMRC, Academia Sinica"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0780","first-page":"289","article-title":"On the foundation of algebraic differential geometry","volume":"2","author":"Wu","year":"1989","journal-title":"Sys. Sci. and Math. Sci."},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0785","first-page":"220","article-title":"On a projection theorem of quasi-varieties in elimination theory","volume":"11B","author":"Wu","year":"1990","journal-title":"Chinese Ann. of Math."},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0790","article-title":"On a finiteness theorem about optimization problems","author":"Wu","year":"1992","journal-title":"Technical Report MM Research Preprints No. 8, MMRC, Academia Sinica"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0795","first-page":"1","article-title":"A report on mechanical geometry theorem proving","volume":"2","author":"Wu","year":"1992","journal-title":"Progress in Natural Sciences"},{"key":"10.1016\/B978-044450813-3\/50013-8_rf0800","article-title":"On surface-fitting problem in CAGD","author":"Wu","year":"1993","journal-title":"Technical Report MM Research Preprints No. 10, MMRC, Academia Sinica"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0805","series-title":"Adg'98, LNAI 1669","first-page":"111","article-title":"A Clifford algebraic method for geometric reasoning","author":"Yang","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0810","series-title":"Proc. of ATCM, (Tsukuba, Japan)","first-page":"24","article-title":"Practical automated reasoning on inequalities","author":"Yang","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0815","series-title":"Proc. of CADE-14, (Townsville, Australia)","first-page":"73","article-title":"A practical symbolic algorithm for inverse kinematics of 6R manipulators with simple geometry","author":"Yang","year":"1997"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0820","series-title":"Automated Deduction in Geometry","first-page":"171","article-title":"Automated proving and discovering of theorems in non-Euclidean geometries","author":"Yang","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0825","series-title":"Adg'98, LNAI 1669","first-page":"30","article-title":"Automated discovering and proving for geometric inequalities","author":"Yang","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0830","first-page":"628","article-title":"A complete discrimination system for polynomials","volume":"E 39","author":"Yang","year":"1996","journal-title":"Sciences in China"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0835","series-title":"Proc. IWMM'92","first-page":"110","article-title":"A criterion of dependency between algebraic equations and its applications","author":"Yang","year":"1992"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0840","series-title":"Non-linear Algebraic Equations and Automated Theorem Proving","author":"Yang","year":"1996"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0845","series-title":"How to Solve Geometry Problems Using Areas","author":"Zhang","year":"1982"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0850","first-page":"109","article-title":"Automated production of traditional proofs for theorems in Euclidean geometry","volume":"13","author":"Zhang","year":"1995","journal-title":"Annals of Math. and AI"},{"key":"10.1016\/B978-044450813-3\/50013-8_bb0855","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1016\/0304-3975(90)90077-U","article-title":"The parallel numerical method of mechanical theorem proving","volume":"74","author":"Zhang","year":"1990","journal-title":"Theoretical Computer Science"}],"container-title":["Handbook of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:B9780444508133500138?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:B9780444508133500138?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,4,29]],"date-time":"2019-04-29T00:54:54Z","timestamp":1556499294000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/B9780444508133500138"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9780444508133"],"references-count":170,"URL":"https:\/\/doi.org\/10.1016\/b978-044450813-3\/50013-8","relation":{},"subject":[],"published":{"date-parts":[[2001]]}}}