{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:07:15Z","timestamp":1762459635812},"reference-count":27,"publisher":"Association for Computing Machinery (ACM)","issue":"6","license":[{"start":{"date-parts":[[2018,11,1]],"date-time":"2018-11-01T00:00:00Z","timestamp":1541030400000},"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":["Form. Asp. Comput."],"published-print":{"date-parts":[[2018,11]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>As robotic systems flourish, reliability has become a topic of paramount importance in the human\u2013robot relationship. The Jacobian matrix in screw theory underpins the design and optimization of robotic manipulators. Kernel properties of robotic manipulators, including dexterity and singularity, are characterized with the Jacobian matrix. The accurate specification and the rigorous analysis of the Jacobian matrix are indispensable in guaranteeing correct evaluation of the kinematics performance of manipulators. In this paper, a formal method for analyzing the Jacobian matrix in screw theory is presented using the higher-order logic theorem prover HOL4. Formalizations of twists and the forward kinematics are performed using the product of exponentials formula and the theory of functional matrices. To the best of our knowledge, this work is the first to formally analyze the kinematic Jacobian using theorem proving. The formal modeling and analysis of the Stanford manipulator demonstrate the effectiveness and applicability of the proposed approach to the formal verification of the kinematic properties of robotic manipulators.<\/jats:p>","DOI":"10.1007\/s00165-018-0468-0","type":"journal-article","created":{"date-parts":[[2018,9,24]],"date-time":"2018-09-24T08:15:31Z","timestamp":1537776931000},"page":"739-757","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Formal analysis of the kinematic Jacobian in screw theory"],"prefix":"10.1145","volume":"30","author":[{"given":"Zhiping","family":"Shi","sequence":"first","affiliation":[{"name":"Beijing Advanced Innovation Center for Imaging Technology, Capital Normal University, Beijing, China"},{"name":"Beijing Center for Mathematics and Information Interdisciplinary Sciences, Capital Normal University, Beijing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Aixuan","family":"Wu","sequence":"additional","affiliation":[{"name":"Beijing Center for Mathematics and Information Interdisciplinary Sciences, Capital Normal University, Beijing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xiumei","family":"Yang","sequence":"additional","affiliation":[{"name":"Beijing Key Laboratory of Light Industrial Robot and Safety Verification, Capital Normal University, Beijing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yong","family":"Guan","sequence":"additional","affiliation":[{"name":"Beijing Advanced Innovation Center for Imaging Technology, Capital Normal University, Beijing, China"},{"name":"Beijing Key Laboratory of Light Industrial Robot and Safety Verification, Capital Normal University, Beijing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yongdong","family":"Li","sequence":"additional","affiliation":[{"name":"Beijing Advanced Innovation Center for Imaging Technology, Capital Normal University, Beijing, China"},{"name":"Beijing Key Laboratory of Light Industrial Robot and Safety Verification, Capital Normal University, Beijing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xiaoyu","family":"Song","sequence":"additional","affiliation":[{"name":"Engineering and Computer Science, Portland State University, Portland, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Affeldt R Cohen C (2017) Formal foundations of 3D geometry to model robot manipulators. In: ACM sigplan conference on certified programs and proofs pp 30\u201342","DOI":"10.1145\/3018610.3018629"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-016-0383-1"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.mechmachtheory.2011.11.015"},{"key":"e_1_2_1_2_4_2","volume-title":"Principles of model checking","author":"Baier C","year":"2008"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"publisher","DOI":"10.1002\/spe.2242"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.mechmachtheory.2012.06.008"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"publisher","DOI":"10.1163\/156855309X462574"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00170-012-4594-1"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","first-page":"347","DOI":"10.1007\/978-3-642-41202-8_23","volume-title":"Formal Methods and Software Engineering","author":"Farooq Binyameen","year":"2013"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"publisher","DOI":"10.1002\/rob.10079"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"publisher","DOI":"10.1115\/1.2801200"},{"key":"e_1_2_1_2_12_2","volume-title":"Introduction to HOL: a theorem proving environment for higher order logic","author":"Gordon MJC","year":"1993"},{"key":"e_1_2_1_2_13_2","first-page":"114","volume-title":"Lecture Notes in Computer Science","author":"Harrison John","year":"2005"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"publisher","DOI":"10.3901\/CJME.2014.01.130"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.mechmachtheory.2011.01.009"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"publisher","DOI":"10.1115\/1.4028622"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"publisher","DOI":"10.5555\/561828"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.mechmachtheory.2014.11.009"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.mechatronics.2015.04.011"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.rcim.2010.12.009"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"Shi Z Liu Z Guan Y Ye S Zhang J Wei H (2014) Formalization of function matrix theory in HOL. J Appl Math 2014","DOI":"10.1155\/2014\/201214"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0263574712000562"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.mechmachtheory.2013.12.007"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"publisher","DOI":"10.1155\/2014\/195276"},{"key":"e_1_2_1_2_25_2","volume-title":"Robot analysis: the mechanics of serial and parallel manipulators","author":"Tsai L-W","year":"1999"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"crossref","unstructured":"Wu A Shi Z Li Y Wu M Guan Y Zhang J Wei H (2015) Formal kinematic analysis of a general 6R manipulator using the screw theory. Math Probl Eng 2015","DOI":"10.1155\/2015\/549797"},{"issue":"1","key":"e_1_2_1_2_27_2","first-page":"1","article-title":"Formalization of linear space theory in the higher-order logic proving system","volume":"2013","author":"Zhang J","year":"2013","journal-title":"J Appl Math"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-018-0468-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-018-0468-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-018-0468-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-018-0468-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T16:22:16Z","timestamp":1641486136000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-018-0468-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,11]]},"references-count":27,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2018,11]]}},"alternative-id":["10.1007\/s00165-018-0468-0"],"URL":"https:\/\/doi.org\/10.1007\/s00165-018-0468-0","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,11]]},"assertion":[{"value":"25 April 2017","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"18 August 2018","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"24 September 2018","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}