{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:48:03Z","timestamp":1749124083451},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540581567"},{"type":"electronic","value":"9783540484677"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-58156-1_28","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T15:22:16Z","timestamp":1330269736000},"page":"401-415","source":"Crossref","is-referenced-by-count":3,"title":["Mechanically proving geometry theorems using a combination of Wu's method and Collins' method"],"prefix":"10.1007","author":[{"given":"Nicholas Freitag","family":"McPhee","sequence":"first","affiliation":[]},{"given":"Shang-Ching","family":"Chou","sequence":"additional","affiliation":[]},{"given":"Xiao-Shan","family":"Gao","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,30]]},"reference":[{"key":"28_CR1","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1016\/0004-3702(88)90049-5","volume":"37","author":"D. S. Arnon","year":"1988","unstructured":"D. S. Arnon. Geometric reasoning with logic and algebra. Artificial Intelligence Journal, 37:37\u201360, 1988.","journal-title":"Artificial Intelligence Journal"},{"key":"28_CR2","volume-title":"PhD thesis","author":"S. C. Chou","year":"1985","unstructured":"S. C. Chou. Proving and discovering theorems in elementary geometries using Wu's method. PhD thesis, Department of Mathematics, University of Texas, Austin, 1985."},{"key":"28_CR3","volume-title":"Mechanical geometry theorem proving","author":"S. C. Chou","year":"1988","unstructured":"S. C. Chou. Mechanical geometry theorem proving. D. Reidel Publishing Company, Dordrecht, Netherlands, 1988."},{"key":"28_CR4","doi-asserted-by":"crossref","unstructured":"S. C. Chou and X. S. Gao. Ritt-Wu's decomposition algorithm and geometry theorem proving. In M. E. Stickel, editor, Proceedings of the 10th international conference on automated deduction. Springer-Verlag, 1990.","DOI":"10.1007\/3-540-52885-7_89"},{"key":"28_CR5","unstructured":"S. C. Chou and X. S. Gao. Techniques for Ritt-Wu's decomposition algorithm. In Proceedings of the IWMM. International Academic Publishing, 1992."},{"key":"28_CR6","volume-title":"Technical Report TR-89-31","author":"S. C. Chou","year":"1989","unstructured":"S. C. Chou, X. S. Gao, and D. S. Arnon. On the mechanical proof of geometry theorems involving inequalities. Technical Report TR-89-31, Department of Computer Sciences, University of Texas at Austin, October 1989."},{"key":"28_CR7","volume-title":"Technical Report TR-89-28","author":"S. C. Chou","year":"1989","unstructured":"S. C. Chou, X. S. Gao, and N. F. McPhee. A combination of Ritt-Wu's method and Collins' method. Technical Report TR-89-28, Department of Computer Sciences, University of Texas at Austin, October 1989."},{"key":"28_CR8","doi-asserted-by":"crossref","unstructured":"G. E. Collins. Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In Proceeding Second GI Conference on Automata Theory and Formal Languages, volume 33 of Lecture Notes In Computer Science, pages 134\u2013183. Springer-Verlag, 1975.","DOI":"10.1007\/3-540-07407-4_17"},{"key":"28_CR9","unstructured":"Hoon Hong. Improvements in CAD-based quantifier elimination. PhD thesis, Computer and Information Science Research Center, The Ohio State University, 1990. Technical Report OSU-CISRC-10\/90-TR29."},{"key":"28_CR10","volume-title":"PhD thesis","author":"N. F. McPhee","year":"1993","unstructured":"Nicholas Freitag McPhee. Mechanically proving geometry theorems using Wu's method and Collins' method. PhD thesis, University of Texas at Austin, 1993."},{"issue":"3","key":"28_CR11","first-page":"207","volume":"4","author":"W. Wen-ts\u00fcn","year":"1984","unstructured":"Wu Wen-ts\u00fcn. Basic principles of mechanical theorem proving in geometries. J. of Sys. Sci. and Math. Sci., 4(3):207\u2013235, 1984. Republished in Journal of Automated Reasoning, 2(4):221\u2013252, 1986.","journal-title":"J. of Sys. Sci. and Math. Sci."},{"issue":"1","key":"28_CR12","first-page":"1","volume":"31","author":"W. Wen-ts\u00fcn","year":"1986","unstructured":"Wu Wen-ts\u00fcn. On zeros of algebraic equations \u2014 an application of Ritt's principle. Kexue Tongbao, 31(1):1\u20135, 1986.","journal-title":"Kexue Tongbao"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2014 CADE-12"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-58156-1_28.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:17:36Z","timestamp":1605647856000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-58156-1_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540581567","9783540484677"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/3-540-58156-1_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}