{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,14]],"date-time":"2026-02-14T09:03:10Z","timestamp":1771059790588,"version":"3.50.1"},"reference-count":31,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2021,4,26]],"date-time":"2021-04-26T00:00:00Z","timestamp":1619395200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,4,26]],"date-time":"2021-04-26T00:00:00Z","timestamp":1619395200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"funder":[{"name":"National Key R&D Program of China","award":["2017YFB1401300"],"award-info":[{"award-number":["2017YFB1401300"]}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2021,8]]},"DOI":"10.1007\/s10817-021-09591-2","type":"journal-article","created":{"date-parts":[[2021,4,26]],"date-time":"2021-04-26T03:14:03Z","timestamp":1619406843000},"page":"711-726","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Automated Discovery of Geometric Theorems Based on Vector Equations"],"prefix":"10.1007","volume":"65","author":[{"given":"Xicheng","family":"Peng","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Qihang","family":"Chen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jingzhong","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2853-2423","authenticated-orcid":false,"given":"Mao","family":"Chen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,4,26]]},"reference":[{"issue":"4","key":"9591_CR1","doi-asserted-by":"publisher","first-page":"802","DOI":"10.1007\/s11424-012-2048-3","volume":"25","author":"JG Jiang","year":"2012","unstructured":"Jiang, J.G., Zhang, J.Z.: A review and prospect of readable machine proofs for geometry theorems. J. Syst. Sci. Complex. 25(4), 802\u2013820 (2012)","journal-title":"J. Syst. Sci. Complex."},{"key":"9591_CR2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-7091-6639-0","volume-title":"Mechanical Theorem Proving in Geometries: Basic Principles","author":"WT Wu","year":"1994","unstructured":"Wu, W.T.: Mechanical Theorem Proving in Geometries: Basic Principles. Springer, New York (1994)"},{"key":"9591_CR3","volume-title":"Mathematics Mechanization","author":"WT Wu","year":"2000","unstructured":"Wu, W.T.: Mathematics Mechanization. Science Press, Kluwer (2000)"},{"key":"9591_CR4","doi-asserted-by":"publisher","DOI":"10.1142\/2196","volume-title":"Machine Proofs in Geometry","author":"SC Chou","year":"1994","unstructured":"Chou, S.C., Gao, X.S., Zhang, J.Z.: Machine Proofs in Geometry. World Scientific, Singapore (1994)"},{"issue":"1","key":"9591_CR5","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0004-3702(75)90013-2","volume":"6","author":"AJ Nevins","year":"1975","unstructured":"Nevins, A.J.: Plane geometry theorem proving using forward chaining. Artif. Intell. 6(1), 1\u201323 (1975)","journal-title":"Artif. Intell."},{"issue":"3","key":"9591_CR6","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1023\/A:1006171315513","volume":"25","author":"SC Chou","year":"2000","unstructured":"Chou, S.C., Gao, X.S., Zhang, J.Z.: A deductive database approach to automated geometry theorem proving and discovering. J. Autom. Reason. 25(3), 219\u2013246 (2000)","journal-title":"J. Autom. Reason."},{"key":"9591_CR7","doi-asserted-by":"publisher","DOI":"10.1142\/6642","volume-title":"Symbolic Computation and Education","author":"SZ Li","year":"2007","unstructured":"Li, S.Z., Wang, D.M., Zhang, J.Z.: Symbolic Computation and Education. World Scientific, Singapore (2007)"},{"issue":"1","key":"9591_CR8","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/s10817-015-9326-4","volume":"55","author":"F Botana","year":"2015","unstructured":"Botana, F., Hohenwarter, M., Janicic, P., Kov\u00e1cs, Z., Petrovi\u0107, I., Recio, T., Weitzhofer, S.: Automated theorem proving in GeoGebra: current achievements. J. Autom. Reason. 55(1), 39\u201359 (2015)","journal-title":"J. Autom. Reason."},{"issue":"3","key":"9591_CR9","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/s10817-009-9162-5","volume":"45","author":"Z Ye","year":"2010","unstructured":"Ye, Z., Chou, S.C., Gao, X.S.: Visually dynamic presentation of proofs in plane geometry. J. Autom. Reason. 45(3), 213\u2013241 (2010)","journal-title":"J. Autom. Reason."},{"key":"9591_CR10","doi-asserted-by":"crossref","unstructured":"Todd, P.: Geometry expressions: a constraint based interactive symbolic geometry system. In: Proc. of the 6th International Workshop on Automated Deduction in Geometry (ADG 2006). LNAI 6877. Springer, Berlin, Heidelberg, New York, pp. 189\u2013202 (2007)","DOI":"10.1007\/978-3-540-77356-6_12"},{"issue":"1\u20133","key":"9591_CR11","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1016\/S0360-1315(01)00089-6","volume":"38","author":"F Botana","year":"2002","unstructured":"Botana, F., Valcarce, J.L.: A dynamic-symbolic interface for geometric theorem discovery. Comput. Educ. 38(1\u20133), 21\u201335 (2002)","journal-title":"Comput. Educ."},{"issue":"1","key":"9591_CR12","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1007\/s11424-019-8350-6","volume":"32","author":"JZ Zhang","year":"2019","unstructured":"Zhang, J.Z., Peng, X.C., Chen, M.: Self-evident automated proving based on point geometry from the perspective of Wu\u2019s method identity. J. Syst. Sci. Complex. 32(1), 78\u201394 (2019)","journal-title":"J. Syst. Sci. Complex."},{"issue":"3","key":"9591_CR13","first-page":"1","volume":"59","author":"Z Jie","year":"2016","unstructured":"Jie, Z., Wang, D., Yao, S.: Automated reducible geometric theorem proving and discovery by Gr\u00f6bner basis method. J. Autom. Reason. 59(3), 1\u201314 (2016)","journal-title":"J. Autom. Reason."},{"key":"9591_CR14","unstructured":"Chou, S.C.: Proving and Discovering Theorems in Elementary Geometries Using Wu\u2019s Method Ph.D. Thesis, Department of Mathematics, University of Texas, Austin (1985)"},{"key":"9591_CR15","doi-asserted-by":"publisher","DOI":"10.1142\/6556","volume-title":"Selected Topics in Geometry with Classical vs. Computer Proving","author":"P Pech","year":"2007","unstructured":"Pech, P.: Selected Topics in Geometry with Classical vs. Computer Proving. World Scientific, Singapore (2007)"},{"issue":"1","key":"9591_CR16","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1023\/A:1006135322108","volume":"23","author":"T Recio","year":"1999","unstructured":"Recio, T., V\u00e9lez, M.P.: Automated discovering of theorems in elementary geometry. J. Autom. Reason. 23(1), 63\u201382 (1999)","journal-title":"J. Autom. Reason."},{"key":"9591_CR17","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1016\/S0747-7171(86)80006-2","volume":"2","author":"B Kutzler","year":"1986","unstructured":"Kutzler, B., Stifter, S.: On the application of Buchberger\u2019s algorithm to automated geometry theorem proving. J. Symb. Comput. 2, 389\u2013397 (1986)","journal-title":"J. Symb. Comput."},{"issue":"19","key":"9591_CR18","first-page":"85","volume":"3","author":"B Buchberger","year":"1995","unstructured":"Buchberger, B., Collins, G., Kutzler, B.: Algebraic methods for geometric reasoning. Annu. Rev. Comput. Sci. 3(19), 85\u2013119 (1995)","journal-title":"Annu. Rev. Comput. Sci."},{"key":"9591_CR19","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-7091-6202-6","volume-title":"Elimination Methods","author":"DM Wang","year":"2001","unstructured":"Wang, D.M.: Elimination Methods. Springer, Wien New York (2001)"},{"key":"9591_CR20","doi-asserted-by":"publisher","DOI":"10.1142\/p318","volume-title":"Elimination Practice. Software Tools and Applications","author":"DM Wang","year":"2004","unstructured":"Wang, D.M.: Elimination Practice. Software Tools and Applications. Imperial College Press, London (2004)"},{"key":"9591_CR21","doi-asserted-by":"crossref","unstructured":"Kapur, D., Saxena, T., Yang, L.: Algebraic and geometric reasoning with dixon resultants. In: Proceedings of International Symposium on Symbolic and Algebraic Computation (Oxford, 1994). ACM Press, New York, pp. 99\u2013107 (1994)","DOI":"10.1145\/190347.190372"},{"issue":"1","key":"9591_CR22","first-page":"10","volume":"15","author":"JZ Zhang","year":"1995","unstructured":"Zhang, J.Z., Yang, L., Hou, X.R.: The sub-resultant method for automated theorem proving. J. Syst. Sci. Math. Sci. 15(1), 10\u201315 (1995)","journal-title":"J. Syst. Sci. Math. Sci."},{"key":"9591_CR23","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-2181-2","volume-title":"Ideals, Varieties and Algorithms, Undergraduate Texts in Mathematics","author":"D Cox","year":"1992","unstructured":"Cox, D., Little, J., O\u2019Shea, D.: Ideals, Varieties and Algorithms, Undergraduate Texts in Mathematics. Springer, Berlin (1992)"},{"key":"9591_CR24","doi-asserted-by":"crossref","unstructured":"Kapur, D.: Automated geometric reasoning: Dixon resultants, Gr\u00f6bner bases, and characteristic sets. In: Automated Deduction in Geometry. LNAI 1360. Springer, pp. 1\u201336 (1997)","DOI":"10.1007\/BFb0022716"},{"issue":"4","key":"9591_CR25","doi-asserted-by":"publisher","first-page":"399","DOI":"10.1016\/S0747-7171(86)80007-4","volume":"2","author":"D Kapur","year":"1986","unstructured":"Kapur, D.: Using Grobner bases to reason about geometry problems. J. Symb. Comput. 2(4), 399\u2013408 (1986)","journal-title":"J. Symb. Comput."},{"key":"9591_CR26","doi-asserted-by":"crossref","unstructured":"Kapur, D.: Geometry theorem proving using Hilbert's Nullstellensatz. In: Proc. of SYMSAC\u201986, Waterloo, pp. 202\u2013208 (1986)","DOI":"10.1145\/32439.32479"},{"key":"9591_CR27","volume-title":"Advanced Euclidean Geometry","author":"RA Johnson","year":"1929","unstructured":"Johnson, R.A.: Advanced Euclidean Geometry. Houghton Mifflin Company, Boston (1929)"},{"key":"9591_CR28","volume-title":"Conics, Books I\u2013III","author":"Apollonius","year":"1997","unstructured":"Apollonius: Conics, Books I\u2013III. Green Lion Press, Santa Fe (1997)"},{"issue":"2","key":"9591_CR29","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1023\/A:1006182023017","volume":"25","author":"H Li","year":"2000","unstructured":"Li, H.: Vectorial equations solving for mechanical geometry theorem proving. J. Autom. Reason. 25(2), 83\u2013121 (2000)","journal-title":"J. Autom. Reason."},{"key":"9591_CR30","doi-asserted-by":"crossref","unstructured":"Chou, S.C., Gao, X.S., Zhang, J.Z.: Mechanical geometry theorem proving by vector calculation. In: Proc. ISSAC93, Kiev. ACM Press, pp. 284\u2013291 (1993)","DOI":"10.1145\/164081.164142"},{"issue":"8","key":"9591_CR31","first-page":"1809","volume":"37","author":"Q Ge","year":"2014","unstructured":"Ge, Q., Zhang, J.Z., Chen, M., Peng, X.C.: Automated geometry readable proving based on vector. Chin. J. Comput. 37(8), 1809\u20131819 (2014)","journal-title":"Chin. J. Comput."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-021-09591-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-021-09591-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-021-09591-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,6,24]],"date-time":"2021-06-24T07:09:54Z","timestamp":1624518594000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-021-09591-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,4,26]]},"references-count":31,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2021,8]]}},"alternative-id":["9591"],"URL":"https:\/\/doi.org\/10.1007\/s10817-021-09591-2","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,4,26]]},"assertion":[{"value":"21 June 2019","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"30 March 2021","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"26 April 2021","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}