{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,16]],"date-time":"2025-01-16T05:30:27Z","timestamp":1737005427321,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540666721"},{"type":"electronic","value":"9783540479970"}],"license":[{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-47997-x_5","type":"book-chapter","created":{"date-parts":[[2007,4,5]],"date-time":"2007-04-05T10:14:18Z","timestamp":1175768058000},"page":"67-85","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Readable Machine Solving in Geometry and ICAI Software MSG"],"prefix":"10.1007","author":[{"given":"Chuan-Zhong","family":"Li","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jhing-Zhong","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2000,11,17]]},"reference":[{"key":"5_CR1","volume-title":"Mechanical geometry theorem proving","author":"S. C. Chou","year":"1988","unstructured":"Chou, S. C., Mechanical geometry theorem proving, D.Reidel Publishing Company, Dordrecht, Netherland, 1988. 67"},{"key":"5_CR2","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. and Zhang, J. Z., Machine proofs in geometry, World Scientific, Singapore, 1994. 67, 68, 70, 76"},{"key":"5_CR3","doi-asserted-by":"crossref","unstructured":"Chou, S. C., Gao, X. S. and Zhang, J. Z., Automated production of traditional proofs for constructive geometry theorems, Proc. of Eighth IEEE Symposium on Logic in Computer Science, pp. 48\u201356, IEEE Computer Society Press, 1993. 70","DOI":"10.1109\/LICS.1993.287601"},{"key":"5_CR4","doi-asserted-by":"crossref","unstructured":"Chou, S. C., Gao, X. S. and Zhang, J. Z., Mechanical geometry theorem proving by vector calculation, Proc. of ISSAC-93, ACM Press, Kiev, pp. 284\u2013291. 70","DOI":"10.1145\/164081.164142"},{"key":"5_CR5","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1007\/BF00283134","volume":"17","author":"S. C. Chou","year":"1996","unstructured":"Chou, S. C., Gao, X. S. and Zhang, J. Z., Automated generation of readable proofs with geometric invariants, II. proving theorems with full-angles, J. of Automated Reasoning, 17, 349\u2013370, 1996. 70","journal-title":"J. of Automated Reasoning"},{"key":"5_CR6","unstructured":"Chou, S. C., Gao, X. S. and Zhang, J. Z., Recent advances of automated geometry theorem proving with high level geometry invariants, Proc. of Asian Symposium on Computer Mathematics, Kobe, Japan, 1996, pp. 173\u2013186. 70"},{"key":"5_CR7","series-title":"TR","volume-title":"Vectors and automated geometry reasoning","author":"S. C. Chou","year":"1994","unstructured":"Chou, S. C., Gao, X. S. and Zhang, J. Z., Vectors and automated geometry reasoning, TR-94-3, CS Dept., WSU, Jan. 1994. 70"},{"key":"5_CR8","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1007\/BF00881858","volume":"14","author":"S. C. Chou","year":"1995","unstructured":"Chou, S. C., Gao, X. S. and Zhang, J. Z., Automated production of traditional proofs in solid geometry, J. Automated Reasoning, 14, 257\u2013291, 1995. 70, 76","journal-title":"J. Automated Reasoning"},{"key":"5_CR9","unstructured":"Chou, S. C., Gao, X. S. and Zhang, J. Z., A fixpoint approach to automated geometry theorem proving, WSUCS-95-2, CS Dept, Wichita State University, 1995 (to appear in J. of Automated Reasoning). 74"},{"key":"5_CR10","unstructured":"Chou, S. C., Gao, X. S. and Zhang, J. Z., The geometry information searching system by forward reasoning, Proc. of Inter. Symposium on Logic and Software Engineering, Beijing, World Scientific, Singapore, 1996. 67, 74"},{"key":"5_CR11","series-title":"TR","volume-title":"A collection of 110 geometry theorems and their machine produced proofs using full-angles","author":"S. C. Chou","year":"1994","unstructured":"Chou, S. C., Gao, X. S. and Zhang, J. Z., A collection of 110 geometry theorems and their machine produced proofs using full-angles, TR-94-4, CS Dept., WSU, March 1994. 76"},{"key":"5_CR12","series-title":"TR","volume-title":"Automated solution of 135 geometry problems from American Mathematical Monthly","author":"S. C. Chou","year":"1994","unstructured":"Chou, S. C., Gao, X. S. and Zhang, J. Z., Automated solution of 135 geometry problems from American Mathematical Monthly, TR-94-8, CS Dept., WSU, August 1994. 76"},{"key":"5_CR13","series-title":"TR","volume-title":"A collection of 90 mechanically solved geometry problems from non-Euclidean geometries","author":"S. C. Chou","year":"1994","unstructured":"Chou, S. C., Gao, X. S. and Zhang, J. Z., A collection of 90 mechanically solved geometry problems from non-Euclidean geometries, TR-94-10, CS Dept., WSU, Oct. 1994. 76"},{"key":"5_CR14","doi-asserted-by":"crossref","unstructured":"Fevre, S. and Wang, D., Proving geometric theorems using Clifford algebra and rewrite rules, Proc. of CADE-15, LNAI 1421, pp. 17\u201332, Springer, 1998. 70","DOI":"10.1007\/BFb0054242"},{"issue":"2","key":"5_CR15","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1145\/356924.356929","volume":"16","author":"H. Gallaire","year":"1984","unstructured":"Gallaire, H., Minker, J. and Nicola, J. M., Logic and databases: a deductive approach, ACM Computing Surveys, 16(2), 153\u2013185, 1984. 74","journal-title":"ACM Computing Surveys"},{"key":"5_CR16","unstructured":"Gao, X. S., Building dynamic mathematical models with Geometry Expert, III. a deductive dabase, Preprint, 1998. 67"},{"key":"5_CR17","unstructured":"Gao, X. S., Zhu, C. C. and Huang, Y., Building dynamic mathematical models with Geometry Expert, I. geometric transformations, functions and plane curves, Proc. of the Third Asian Technology Conference in Mathematics, Ed. W. C. Yang, pp. 216\u2013224, Springer, 1998. 67"},{"key":"5_CR18","unstructured":"Gao, X. S., Zhu, C. C. and Huang, Y., Building dynamic mathematical models with Geometry Expert, II. linkages. Proc. of the Third Asian Symposium on Computer Mathematics, Ed. Z. B. Li, pp. 15\u201322, Lanzhou University Press, 1998. 67"},{"key":"5_CR19","volume-title":"Geometry Expert (Chinese book with software)","author":"X. S. Gao","year":"1998","unstructured":"Gao, X. S., Zhang, J. Z. and Chou, S. C., Geometry Expert (Chinese book with software), Chiu Chang Mathematics Publishers, Taipei, 1998."},{"key":"5_CR20","doi-asserted-by":"crossref","unstructured":"Gelernter, H., Hanson, J. R. and Loveland, D. W., Empirical explorations of the geometry-theorem proving machine, Proc. West. Joint Computer Conf., pp. 143\u2013147, 1960. 67, 75","DOI":"10.1145\/1460361.1460381"},{"key":"5_CR21","volume-title":"MathLab: solid geometry","author":"C. Z. Li","year":"1998","unstructured":"Li, C. Z. and Zhang, J. Z., MathLab: solid geometry (Chinese book with software), China Juvenile Publishers, Beijing, 1998. 76"},{"key":"5_CR22","unstructured":"Li, H. (1996): Clifford algebra and area method. MM-Research Preprints No. bf 14, pp. 37\u201369, Institute of Systems Science, Academia Sinica, 1996. 70"},{"key":"5_CR23","doi-asserted-by":"publisher","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, Artificial Intelligence, 6, 1\u201323, 1975. 74, 75","journal-title":"Artificial Intelligence"},{"issue":"4","key":"5_CR24","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1109\/TC.1976.1674613","volume":"C-25","author":"R. Reiter","year":"1976","unstructured":"Reiter, R., A semantically guided deductive system for automatic theorem proving, IEEE Tras. on Computers, C-25(4), 328\u2013334, 1976. 74","journal-title":"IEEE Tras. on Computers"},{"key":"5_CR25","doi-asserted-by":"crossref","unstructured":"Robinson, A., Proving a theorem (as done by man, logician, or machine), Automation of Reasoning, Ed. J. Siekmann and G. Wrightson, pp. 74\u201378, Springer, 1983. 74","DOI":"10.1007\/978-3-642-81952-0_5"},{"key":"5_CR26","unstructured":"Stifter, S. (1993): Geometry theorem proving in vector spaces by means of gr\u00f6bner bases, Proc. of ISSAC-93, Kiev, pp. 301\u2013310, ACM Press, 1993. 70"},{"key":"5_CR27","doi-asserted-by":"crossref","unstructured":"Wang, D., Clifford algebraic calculus for geometric reasoning with application to computer system vision, Automated Deduction in Geometry, Ed. D. Wang, LNAI 1360, pp. 115\u2013140, Springer, 1997. 70","DOI":"10.1007\/BFb0022723"},{"key":"5_CR28","doi-asserted-by":"crossref","unstructured":"Wu, W. T., On the decision problem and the mechanization of theorem-proving in elementary geometry, Scientia Sinica, 21, 159\u2013172. Re-published in Automated Theorem Proving: after 25 Years, Ed.W.W. Bledsoe and D.W. Loveland, pp. 235\u2013242, 1984. 67","DOI":"10.1090\/conm\/029\/12"},{"key":"5_CR29","doi-asserted-by":"crossref","unstructured":"Yang, L., Gao, X. S., Chou, S. C. and Zhang, J. Z., Automated production of readable proofs for theorems in non-Euclidean geometries, Automated Deduction in Geometry, Ed. D. Wang, LNAI 1360, pp. 171\u2013188, Springer, 1997. 67, 70","DOI":"10.1007\/BFb0022725"},{"key":"5_CR30","unstructured":"Yang, H. Q., Zhang, S. G. and Feng, G. C., Clifford algebra and mechanical geometry theorem proving, Proc. of the Third Asian Symposium on Computer Mathematics, Ed. Z. B. Li, pp. 49\u201364, Lanzhou University Press, 1998. 70"},{"key":"5_CR31","first-page":"109","volume":"13","author":"J. Z. Zhang","year":"1992","unstructured":"Zhang, J. Z., Chou, S. C. and Gao, X. S., Automated production of traditional proofs for theorems in Euclidean geometry, I. the Hilbert intersection point theorems, TR-92-3, CS Dept., WSU, 1992. Also in Annals of Mathematics and AI, 13, 109\u2013137, 1995. 67, 68, 70","journal-title":"Annals of Mathematics and AI"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction in Geometry"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-47997-X_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,15]],"date-time":"2025-01-15T14:25:42Z","timestamp":1736951142000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-47997-X_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540666721","9783540479970"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/3-540-47997-x_5","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]},"assertion":[{"value":"17 November 2000","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}