{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,20]],"date-time":"2026-03-20T16:56:09Z","timestamp":1774025769890,"version":"3.50.1"},"reference-count":30,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2016,11,22]],"date-time":"2016-11-22T00:00:00Z","timestamp":1479772800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100001809","name":"National Nature Science Foundation of China","doi-asserted-by":"crossref","award":["11301523"],"award-info":[{"award-number":["11301523"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100001809","name":"National Nature Science Foundation of China","doi-asserted-by":"crossref","award":["11371356"],"award-info":[{"award-number":["11371356"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2017,10]]},"DOI":"10.1007\/s10817-016-9395-z","type":"journal-article","created":{"date-parts":[[2016,11,22]],"date-time":"2016-11-22T17:54:06Z","timestamp":1479837246000},"page":"331-344","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Automated Reducible Geometric Theorem Proving and Discovery by Gr\u00f6bner Basis Method"],"prefix":"10.1007","volume":"59","author":[{"given":"Jie","family":"Zhou","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dingkang","family":"Wang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yao","family":"Sun","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,11,22]]},"reference":[{"key":"9395_CR1","doi-asserted-by":"crossref","unstructured":"Gelernter, H., Hanson, J.R., Loveland, D.W.: Empirical explorations of the geometry-theorem proving machine. In: Proceeding of the West Joint Computer Conference, pp. 143\u2013147 (1960)","DOI":"10.1145\/1460361.1460381"},{"key":"9395_CR2","first-page":"24","volume":"35","author":"A Tarski","year":"1951","unstructured":"Tarski, A.: A decision method for elementary algebra and geometry. Texts Monogr. Symb. Comput. 35, 24\u201384 (1951)","journal-title":"Texts Monogr. Symb. Comput."},{"issue":"2","key":"9395_CR3","doi-asserted-by":"crossref","first-page":"365","DOI":"10.2307\/1969640","volume":"60","author":"A Seidenberg","year":"1954","unstructured":"Seidenberg, A.: A new decision method for elememtary algebra. Ann. Math. 60(2), 365\u2013374 (1954)","journal-title":"Ann. Math."},{"key":"9395_CR4","doi-asserted-by":"crossref","unstructured":"Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decomposition. Quantifier Elimination and Cylindrical Algebraic Decomposition, pp. 85\u2013121. Springer, Vienna (1998)","DOI":"10.1007\/978-3-7091-9459-1_4"},{"key":"9395_CR5","first-page":"159","volume":"21","author":"WT Wu","year":"1978","unstructured":"Wu, W.T.: On the decision problem and the mechanization of theorem proving in elementary geometry. Sci. Sin. 21, 159\u2013172 (1978)","journal-title":"Sci. Sin."},{"issue":"3","key":"9395_CR6","doi-asserted-by":"crossref","first-page":"221","DOI":"10.1007\/BF02328447","volume":"2","author":"WT Wu","year":"1986","unstructured":"Wu, W.T.: Basic principles of mechanical theorem proving in elementary geometries. J. Autom. Reason. 2(3), 221\u2013252 (1986)","journal-title":"J. Autom. Reason."},{"key":"9395_CR7","volume-title":"Mechanical Geometry Theorem Proving, Mathematics and Its Applications","author":"SC Chou","year":"1988","unstructured":"Chou, S.C.: Mechanical Geometry Theorem Proving, Mathematics and Its Applications. Reidel, Amsterdam (1988)"},{"key":"9395_CR8","doi-asserted-by":"crossref","unstructured":"Ritt, J.F.: Differential equations from the algebraic standpoint. Am. Math. Soc. (1932)","DOI":"10.1090\/coll\/014"},{"issue":"3","key":"9395_CR9","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1007\/BF02328448","volume":"2","author":"SC Chou","year":"1986","unstructured":"Chou, S.C.: Proving geometry theorems with rewrite rules. J. Autom. Reason. 2(3), 253\u2013273 (1986)","journal-title":"J. Autom. Reason."},{"key":"9395_CR10","doi-asserted-by":"crossref","unstructured":"Kapur, D.: Geometry theorem proving using Hilbert\u2019s Nullstellensatz. In: Proceedings of the ISSAC, pp. 202\u2013208. ACM Press, New York (1986)","DOI":"10.1145\/32439.32479"},{"key":"9395_CR11","doi-asserted-by":"crossref","unstructured":"Kutzler, B., Stifter, S.: Automated geometry theorem proving using Buchberger\u2019s algorithm. In: Proceedings of ISSAC, pp. 209\u2013214. ACM Press, New York (1986)","DOI":"10.1145\/32439.32480"},{"key":"9395_CR12","volume-title":"Introduction to Geometry","author":"HSM Coxeter","year":"1961","unstructured":"Coxeter, H.S.M.: Introduction to Geometry. Wiley, New York (1961)"},{"key":"9395_CR13","first-page":"484","volume":"90","author":"KB Taylor","year":"1983","unstructured":"Taylor, K.B.: Three circles with collinear centers. Am. Math. Mon. 90, 484\u2013486 (1983)","journal-title":"Am. Math. Mon."},{"issue":"2","key":"9395_CR14","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1007\/s10817-009-9133-x","volume":"43","author":"G Dalzotto","year":"2009","unstructured":"Dalzotto, G., Recio, T.: On protocols for the automated discovery of theorems in elementary geometry. J. Autom. Reason. 43(2), 203\u2013236 (2009)","journal-title":"J. Autom. Reason."},{"key":"9395_CR15","unstructured":"Botana, F., Montes, A., Recio, T.: An algorithm for automatic discovery of algebraic loci. In: Proceedings of the ADG, pp. 53\u201359 (2012)"},{"key":"9395_CR16","doi-asserted-by":"crossref","unstructured":"Chen, X.F., Li, P., Lin, L., Wang, D.K.: Proving geometric theorems by partitioned-parametric Gr\u00f6bner bases. In: Proceedings of the ADG, pp. 34\u201343 (2004)","DOI":"10.1007\/11615798_3"},{"key":"9395_CR17","doi-asserted-by":"crossref","unstructured":"Montes, A., Recio, T.: Automatic discovery of geometry theorems using minimal canonical comprehensive Gr\u00f6bner systems. In: Proceedings of the ADG, pp. 113\u2013138 (2006)","DOI":"10.1007\/978-3-540-77356-6_8"},{"issue":"1","key":"9395_CR18","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1023\/A:1006135322108","volume":"23","author":"T Recio","year":"1999","unstructured":"Recio, T., Velez, M.P.: Automatic discovery of theorems in elementary geometry. J. Autom. Reason. 23(1), 63\u201382 (1999)","journal-title":"J. Autom. Reason."},{"key":"9395_CR19","unstructured":"Wang, D.K., Lin, L.: Automatic discovery of geometric theorem by computing Gr\u00f6bner bases with parameters. In: Abstracts of Presentations of ACA, vol. 32, Japan (2005)"},{"issue":"1","key":"9395_CR20","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. Pannon. 1(1), 15\u201332 (1990)","journal-title":"Math. Pannon."},{"issue":"1","key":"9395_CR21","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0747-7171(92)90023-W","volume":"14","author":"V Weispfenning","year":"1992","unstructured":"Weispfenning, V.: Comprehensive Gr\u00f6bner bases. J. Symb. Comput. 14(1), 1\u201329 (1992)","journal-title":"J. Symb. Comput."},{"key":"9395_CR22","unstructured":"Kapur, D.: An approach for solving systems of parametric polynomial equations. In: Saraswat, V., Van Hentenryck, (eds.) Principles and Practices of Constraints Programming, pp. 217\u2013244. MIT Press, Cambridge (1995)"},{"key":"9395_CR23","doi-asserted-by":"crossref","unstructured":"Kapur, D., Sun, Y., Wang, D.K.: A new algorithm for computing comprehensive Gr\u00f6bner systems. In: Proceedings of the ISSAC, pp. 29\u201336. ACM Press, New York (2010)","DOI":"10.1145\/1837934.1837946"},{"issue":"2","key":"9395_CR24","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1006\/jsco.2001.0504","volume":"33","author":"A Montes","year":"2002","unstructured":"Montes, A.: A new algorithm for discussing Gr\u00f6bner bases with parameters. J. Symb. Comput. 33(2), 183\u2013208 (2002)","journal-title":"J. Symb. Comput."},{"issue":"12","key":"9395_CR25","doi-asserted-by":"crossref","first-page":"1391","DOI":"10.1016\/j.jsc.2010.06.017","volume":"45","author":"A Montes","year":"2010","unstructured":"Montes, A., Wibmer, M.: Gr\u00f6bner bases for polynomial systems with parameters. J. Symb. Comput. 45(12), 1391\u20131425 (2010)","journal-title":"J. Symb. Comput."},{"key":"9395_CR26","doi-asserted-by":"crossref","unstructured":"Nabeshima, K.: A speed-up of the algorithm for computing comprehensive Gr\u00f6bner systems. In: Proceedings of the ISSAC, pp. 299\u2013306. ACM Press, New York (2007)","DOI":"10.1145\/1277548.1277589"},{"issue":"3","key":"9395_CR27","doi-asserted-by":"crossref","first-page":"649","DOI":"10.1016\/S0747-7171(03)00098-1","volume":"36","author":"A Suzuki","year":"2003","unstructured":"Suzuki, A., Sato, Y.: An alternative approach to comprehensive Gr\u00f6bner bases. J. Symb. Comput. 36(3), 649\u2013667 (2003)","journal-title":"J. Symb. Comput."},{"issue":"3","key":"9395_CR28","doi-asserted-by":"crossref","first-page":"669","DOI":"10.1016\/S0747-7171(03)00099-3","volume":"36","author":"V Weispfenning","year":"2003","unstructured":"Weispfenning, V.: Canonical comprehensive Gr\u00f6bner bases. J. Symb. Comput. 36(3), 669\u2013683 (2003)","journal-title":"J. Symb. Comput."},{"issue":"5","key":"9395_CR29","doi-asserted-by":"crossref","first-page":"463","DOI":"10.1016\/j.jsc.2007.07.022","volume":"44","author":"M Manubens","year":"2009","unstructured":"Manubens, M., Montes, A.: Minimal canonical comprehensive Groebner system. J. Symb. Comput. 44(5), 463\u2013478 (2009)","journal-title":"J. Symb. Comput."},{"key":"9395_CR30","doi-asserted-by":"crossref","DOI":"10.1007\/978-0-387-35651-8","volume-title":"Ideals, Varieties, and Algorithms","author":"D Cox","year":"2007","unstructured":"Cox, D., Little, J., O\u2019Shea, D.: Ideals, Varieties, and Algorithms, 3rd edn. Springer, New York (2007)","edition":"3"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-016-9395-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-016-9395-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-016-9395-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,12]],"date-time":"2025-06-12T20:24:18Z","timestamp":1749759858000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-016-9395-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,11,22]]},"references-count":30,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2017,10]]}},"alternative-id":["9395"],"URL":"https:\/\/doi.org\/10.1007\/s10817-016-9395-z","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,11,22]]}}}