{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,25]],"date-time":"2026-01-25T15:16:55Z","timestamp":1769354215059,"version":"3.49.0"},"reference-count":30,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2019,2,1]],"date-time":"2019-02-01T00:00:00Z","timestamp":1548979200000},"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":["J Syst Sci Complex"],"published-print":{"date-parts":[[2019,2]]},"DOI":"10.1007\/s11424-019-8354-2","type":"journal-article","created":{"date-parts":[[2019,2,14]],"date-time":"2019-02-14T00:53:25Z","timestamp":1550105605000},"page":"95-123","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Automated Theorem Proving Practice with Null Geometric Algebra"],"prefix":"10.1007","volume":"32","author":[{"given":"Hongbo","family":"Li","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,2,14]]},"reference":[{"key":"8354_CR1","volume-title":"Basic Principles of Mechanical Theorem Proving in Geometries I: Part of Elementary Geometries","author":"W T Wu","year":"1984","unstructured":"Wu W T, Basic Principles of Mechanical Theorem Proving in Geometries I: Part of Elementary Geometries, Science Press, Beijing, 1984; Springer, Wien, 1994."},{"key":"8354_CR2","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 and Stifter S, On the application of Buchberger\u2019s algorithm to automated geometry theorem proving, J. Symb. Comp., 1986, 2: 389\u2013398.","journal-title":"J. Symb. Comp."},{"key":"8354_CR3","first-page":"107","volume-title":"Invariant Methods in Discrete and Computational Geometry","author":"H Crapo","year":"1994","unstructured":"Crapo H and Richter-Gebert J, Automatic proving of geometric theorems, Invariant Methods in Discrete and Computational Geometry, Ed. by White N, Kluwer Academic Publishers, 1994, 107\u2013139."},{"key":"8354_CR4","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-7091-6202-6","volume-title":"Elimination Methods","author":"D Wang","year":"2001","unstructured":"Wang D, Elimination Methods, Springer, Wien, New York, 2001."},{"key":"8354_CR5","volume-title":"Mechanical Geometry Theorem Proving","author":"S C Chou","year":"1988","unstructured":"Chou S C, Mechanical Geometry Theorem Proving, D. Reidel, Dordrecht, 1988."},{"key":"8354_CR6","first-page":"35","volume-title":"Mathematical Aspects of Computer and Information Sciences","author":"H Li","year":"2015","unstructured":"Li H, Symbolic geometric reasoning with advanced invariant algebras, Mathematical Aspects of Computer and Information Sciences, Eds. by Kotsireas I S, et al., LNCS 9582, Springer Switzerland, 2015, 35\u201349."},{"key":"8354_CR7","unstructured":"Richter-Gebert J and Li H, Coordinate-free theorem proving in incidence geometry, Eds. by Sitharam M, et al., Handbook of Geometric Constraint Systems Principles, CRC Press, Boca Raton, 2019, 59\u201382."},{"key":"8354_CR8","first-page":"261","volume-title":"Proc. ISSAC 2007","author":"H Li","year":"2007","unstructured":"Li H, A recipe for symbolic geometric computing: Long geometric product, breefs and Clifford factorization, Ed. by Brown C W, Proc. ISSAC 2007, ACM Press, New York, 2007, 261\u2013268."},{"key":"8354_CR9","first-page":"106","volume-title":"Handbook of Geometric Constraint Systems Principles","author":"T F Havel","year":"2019","unstructured":"Havel T F and Li H, From molecular distance geometry to conformal geometric algebra, Eds. by Sitharam M, et al., Handbook of Geometric Constraint Systems Principles, CRC Press, Boca Raton, 2019, 106\u2013136."},{"key":"8354_CR10","volume-title":"Acad. Math. and Sys. Sci.","author":"N Cao","year":"2006","unstructured":"Cao N, Geometric decomposition based on conformal geometric algebra and its program realization, PhD Dissertation, Acad. Math. and Sys. Sci., Chinese Academy of Sciences, Beijing, 2006."},{"key":"8354_CR11","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/978-0-85729-811-9_10","volume-title":"Guide to Geometric Algebra in Practice","author":"H Li","year":"2011","unstructured":"Li H and Cao Y, On geometric theorem proving with null geometric algebra, Eds. by Dorst L and Lasenby J, Guide to Geometric Algebra in Practice, Springer, London, 2011, 195\u2013216."},{"key":"8354_CR12","doi-asserted-by":"publisher","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."},{"key":"8354_CR13","first-page":"221","volume-title":"Proc. ISSAC 2004","author":"H Li","year":"2004","unstructured":"Li H, Symbolic computation in the homogeneous geometric model with Clifford algebra, Ed. by Gutierrez J, Proc. ISSAC 2004, ACM Press, New York, 2004, 221\u2013228."},{"key":"8354_CR14","first-page":"6","volume-title":"Proc. ATCM 2006","author":"H Li","year":"2006","unstructured":"Li H, Geometric reasoning with invariant algebras, Proc. ATCM 2006, ATCM Inc., Blacksburg, USA, 2006, 6\u201319."},{"issue":"9","key":"8354_CR15","first-page":"1189","volume":"29","author":"Y Cao","year":"2009","unstructured":"Cao Y and Li H, Elimination and simplification algorithms in geometric algebra for theorem proving, J. Sys. Sci. Math., 2009, 29(9): 1189\u20131199 (in Chinese).","journal-title":"J. Sys. Sci. Math."},{"key":"8354_CR16","first-page":"7","volume-title":"Proc. ISSAC 2017","author":"H Li","year":"2015","unstructured":"Li H, Automated geometric reasoning with geometric algebra: Theory and practice, Proc. ISSAC 2017, 2015, 7\u20138, Slides: http:\/\/www.issac-conference.org\/2017\/assets\/tutorial slides\/Li.pdf."},{"key":"8354_CR17","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-009-6292-7","volume-title":"Clifford Algebra to Geometric Calculus","author":"D Hestenes","year":"1984","unstructured":"Hestenes D and Sobczyk G, Clifford Algebra to Geometric Calculus, Kluwer, Dordrecht, 1984."},{"key":"8354_CR18","doi-asserted-by":"publisher","DOI":"10.1142\/6514","volume-title":"Invariant Algebras and Geometric Reasoning","author":"H Li","year":"2008","unstructured":"Li H, Invariant Algebras and Geometric Reasoning, World Scientific, Singapore, 2008."},{"key":"8354_CR19","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-88-470-2107-5_9","volume-title":"Algebraic Combinatorics and Computer Science","author":"A Brini","year":"2001","unstructured":"Brini A, Regonati F, and Teolis A G B, Grassmann Geometric Calculus, Invariant Theory and Superalgebras, Eds. by Crapo H and Senato D, Algebraic Combinatorics and Computer Science, Springer, Milano, 2001, 151\u2013196."},{"key":"8354_CR20","volume-title":"Combinatorics and Renormalization in Quantum Field Theory","author":"E Caianiello","year":"1973","unstructured":"Caianiello E, Combinatorics and Renormalization in Quantum Field Theory, Benjamin, Reading, 1973."},{"key":"8354_CR21","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/978-1-4612-0089-5_5","volume-title":"Applications of Geometric Algebra in Computer Science and Engineering","author":"H Li","year":"2002","unstructured":"Li H, Automated theorem proving in the homogeneous model with Clifford bracket algebra, Applications of Geometric Algebra in Computer Science and Engineering, Eds. by Dorst L, et al., Birkh\u00e4user, Boston, 2002, 69\u201378."},{"key":"8354_CR22","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1007\/978-3-0348-7838-8_17","volume-title":"Trends in Mathematics: Advances in Analysis and Geometry","author":"H Li","year":"2004","unstructured":"Li H, Automated geometric theorem proving, clifford bracket algebra and Clifford expansions, Eds. by Qian T, et al., Trends in Mathematics: Advances in Analysis and Geometry, Birkh\u00e4user, Basel, 2004, 345\u2013363."},{"key":"8354_CR23","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/978-94-015-8402-9_11","volume-title":"Invariant Methods in Discrete and Computational Geometry","author":"T F Havel","year":"1995","unstructured":"Havel T F, Geometric algebra and M\u00f6bius sphere geometry as a basis for Euclidean invariant theory, Ed. by White N, Invariant Methods in Discrete and Computational Geometry, D. Reidel, Dordrecht, 1995, 245\u2013256."},{"key":"8354_CR24","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1007\/978-3-662-04621-0_2","volume-title":"Geometric Computing with Clifford Algebras","author":"H Li","year":"2001","unstructured":"Li H, Hestenes D, and Rockwood A, Generalized homogeneous coordinates for computational geometry, Geometric Computing with Clifford Algebras, Ed. by Sommer G, Springer, Heidelberg, 2001, 27\u201360."},{"key":"8354_CR25","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-4096-7","volume-title":"Lie Sphere Geometry","author":"T E Cecil","year":"1992","unstructured":"Cecil T E, Lie Sphere Geometry, Springer, New York, 1992."},{"key":"8354_CR26","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/978-0-85729-811-9_13","volume-title":"Guide to Geometric Algebra in Practice","author":"H Li","year":"2011","unstructured":"Li H and Zhang L, Line geometry in terms of the null geometric algebra over R3,3, and application to the inverse singularity analysis of generalized stewart platforms, Eds. by Dorst L and Lasenby J, Guide to Geometric Algebra in Practice, Springer, London, 2011, 253\u2013272."},{"key":"8354_CR27","first-page":"181","volume-title":"Proc. ISSAC 2008","author":"H Li","year":"2008","unstructured":"Li H and Huang L, Complex brackets, balanced complex differences, and applications in symbolic geometric computing, Proc. ISSAC 2008, ACM Press, New York, 2008, 181\u2013188."},{"issue":"8","key":"8354_CR28","first-page":"915","volume":"28","author":"H Li","year":"2008","unstructured":"Li H, From geometric algebra to advanced invariant computing, J. Sys. Sci. Math., 2008, 28(8): 915\u2013929 (in Chinese).","journal-title":"J. Sys. Sci. Math."},{"key":"8354_CR29","first-page":"195","volume-title":"Proc. AGACSE\u201915","author":"H Li","year":"2015","unstructured":"Li H, Huang L, Dong L, et al., Elements of line geometry with geometric algebra, Proc. AGACSE\u201915, Eds. by Descamps S X, et al., FIB Barcelona, 2015, 195\u2013204. Full version: arXiv: 1507.06634 [math.MG]."},{"key":"8354_CR30","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/10722492_7","volume-title":"Algebraic Frames for the Perception-Action Cycle","author":"H Li","year":"2000","unstructured":"Li H, The Lie model for Euclidean geometry, Eds. by Sommer G and Zeevi Y, Algebraic Frames for the Perception-Action Cycle, LNCS 1888, Springer, Berlin, 2000, 115\u2013133."}],"container-title":["Journal of Systems Science and Complexity"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11424-019-8354-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11424-019-8354-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11424-019-8354-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,2,13]],"date-time":"2020-02-13T19:05:21Z","timestamp":1581620721000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11424-019-8354-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,2]]},"references-count":30,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2019,2]]}},"alternative-id":["8354"],"URL":"https:\/\/doi.org\/10.1007\/s11424-019-8354-2","relation":{},"ISSN":["1009-6124","1559-7067"],"issn-type":[{"value":"1009-6124","type":"print"},{"value":"1559-7067","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,2]]},"assertion":[{"value":"31 August 2018","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"30 November 2018","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"14 February 2019","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}