{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:35:18Z","timestamp":1740123318087,"version":"3.37.3"},"reference-count":38,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2020,3,6]],"date-time":"2020-03-06T00:00:00Z","timestamp":1583452800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,3,6]],"date-time":"2020-03-06T00:00:00Z","timestamp":1583452800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"name":"National Key R & D Pla","award":["2017YFB1303000"],"award-info":[{"award-number":["2017YFB1303000"]}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["61876111","61572331"],"award-info":[{"award-number":["61876111","61572331"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["61602325","61877040"],"award-info":[{"award-number":["61602325","61877040"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2021,1]]},"DOI":"10.1007\/s10817-020-09549-w","type":"journal-article","created":{"date-parts":[[2020,3,6]],"date-time":"2020-03-06T17:02:31Z","timestamp":1583514151000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Formalization of Euler\u2013Lagrange Equation Set Based on Variational Calculus in HOL Light"],"prefix":"10.1007","volume":"65","author":[{"given":"Yong","family":"Guan","sequence":"first","affiliation":[]},{"given":"Jingzhi","family":"Zhang","sequence":"additional","affiliation":[]},{"given":"Guohui","family":"Wang","sequence":"additional","affiliation":[]},{"given":"Ximeng","family":"Li","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3562-8602","authenticated-orcid":false,"given":"Zhiping","family":"Shi","sequence":"additional","affiliation":[]},{"given":"Yongdong","family":"Li","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,3,6]]},"reference":[{"unstructured":"Adnan, R., Osman, H.: Formal analysis of robotic cell injection systems using theorem proving. In: Conference on Intelligent Computer Mathematics, pp. 1\u20139. RISC, Hagenberg (2018). https:\/\/arxiv.org\/pdf\/1807.07378.pdf","key":"9549_CR1"},{"issue":"1","key":"9549_CR2","doi-asserted-by":"publisher","first-page":"368","DOI":"10.1016\/S0022-247X(02)00180-4","volume":"272","author":"O Agrawal","year":"2002","unstructured":"Agrawal, O.: Formulation of Euler\u2013Lagrange equations for fractional variational problems. J. Math. Anal. Appl. 272(1), 368\u2013379 (2002)","journal-title":"J. Math. Anal. Appl."},{"unstructured":"Binyameen, F., Osman, H., Sohail, I.: Formal kinematic analysis of the two-link planar manipulator. In: International Conference on Formal Engineering Methods (2013)","key":"9549_CR3"},{"doi-asserted-by":"crossref","unstructured":"Blanchette, J.C., Bulwahn, L., Nipkow, T.: Automatic proof and disproof in Isabelle\/HOL. In: International Conference on Frontiers of Combining Systems, pp. 12\u201327 (2011)","key":"9549_CR4","DOI":"10.1007\/978-3-642-24364-6_2"},{"key":"9549_CR5","volume-title":"Lectures on the Calculus of Variations","author":"GA Bliss","year":"1946","unstructured":"Bliss, G.A.: Lectures on the Calculus of Variations. The University of Chicago Press, Chicago (1946)"},{"issue":"7","key":"9549_CR6","doi-asserted-by":"publisher","first-page":"1196","DOI":"10.1017\/S0960129514000437","volume":"26","author":"S Boldo","year":"2016","unstructured":"Boldo, S., Lelay, C., Melquiond, G.: Formalization of real analysis: a survey of proof assistants and libraries. Math. Struct. Comput. Sci. 26(7), 1196\u20131233 (2016)","journal-title":"Math. Struct. Comput. Sci."},{"key":"9549_CR7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-06074-3_9","volume-title":"Basic Concepts on the Calculus of Variations","author":"F Botelho","year":"2014","unstructured":"Botelho, F.: Basic Concepts on the Calculus of Variations. Springer International Publishing, Cham (2014)"},{"unstructured":"Ferguson, J.: A brief survey of the history of the calculus of variations and its applications. Mathematics 1\u201326 (2004)","key":"9549_CR8"},{"issue":"1","key":"9549_CR9","doi-asserted-by":"publisher","first-page":"81","DOI":"10.3103\/S1066369X17010108","volume":"61","author":"KG Garaev","year":"2017","unstructured":"Garaev, K.G., Aksent\u2019Ev, L.A.: A problem on brachistochrone as invariant variational problem. Russ. Math. 61(1), 81\u201384 (2017)","journal-title":"Russ. Math."},{"key":"9549_CR10","volume-title":"Calculus of Variations (translated by R. A. Silverman)","author":"IM Gelfand","year":"1963","unstructured":"Gelfand, I.M., Fomin, S.V.: Calculus of Variations (translated by R. A. Silverman). Prentice-Hall, Upper Saddle River (1963)"},{"issue":"6","key":"9549_CR11","doi-asserted-by":"publisher","first-page":"993","DOI":"10.1007\/s00165-012-0232-9","volume":"25","author":"H Gottliebsen","year":"2013","unstructured":"Gottliebsen, H., Hardy, R., Lightfoot, O., Martin, U.: Applications of real number theorem proving in PVS. Form. Asp. Comput. 25(6), 993\u20131016 (2013)","journal-title":"Form. Asp. Comput."},{"issue":"1","key":"9549_CR12","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1016\/0022-1236(82)90088-X","volume":"49","author":"EP Hamilton","year":"1982","unstructured":"Hamilton, E.P., Nashed, M.Z.: Global and local variational derivatives and integral representations of G\u00e2utex differentials. J. Funct. Anal. 49(1), 128\u2013144 (1982)","journal-title":"J. Funct. Anal."},{"doi-asserted-by":"crossref","unstructured":"Harrison, J.: HOL Light: an overview. In: International Conference on Theorem Proving in Higher Order Logics, pp. 60\u201366 (2009)","key":"9549_CR13","DOI":"10.1007\/978-3-642-03359-9_4"},{"issue":"2","key":"9549_CR14","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/s10817-012-9250-9","volume":"50","author":"J Harrison","year":"2013","unstructured":"Harrison, J.: The HOL Light theory of Euclidean space. J. Autom. Reason. 50(2), 173\u2013190 (2013)","journal-title":"J. Autom. Reason."},{"issue":"4","key":"9549_CR15","doi-asserted-by":"publisher","first-page":"847","DOI":"10.1016\/S0960-0779(03)00265-0","volume":"19","author":"JH He","year":"2004","unstructured":"He, J.H.: Variational principles for some nonlinear partial differential equations with variable coefficients. Chaos Solitons Fractals 19(4), 847\u2013851 (2004)","journal-title":"Chaos Solitons Fractals"},{"unstructured":"Harrison, J., Maggesi, M.: HOL Light Vector and Matrice (2019). https:\/\/github.com\/jrh13\/hol-light\/tree\/master\/Multivariate\/vectors.ml","key":"9549_CR16"},{"unstructured":"Harrison, J., Bruno, V., Maggesi, M.: HOL Light Topology (2019). https:\/\/github.com\/jrh13\/hol-light\/tree\/master\/Multivariate\/topology.ml","key":"9549_CR17"},{"unstructured":"Harrison, J., Maggesi, M.: HOL Light Metric (2019). https:\/\/github.com\/jrh13\/hol-light\/tree\/master\/Multivariate\/metric.ml","key":"9549_CR18"},{"unstructured":"Harrison, J., Maggesi, M.: HOL Light Integral (2019). https:\/\/github.com\/jrh13\/hol-light\/tree\/master\/Multivariate\/integral.ml","key":"9549_CR19"},{"unstructured":"Harrison, J., Maggesi, M.: HOL Light Derivative (2019). https:\/\/github.com\/jrh13\/hol-light\/tree\/master\/Multivariate\/derivative.ml","key":"9549_CR20"},{"unstructured":"Harrison, J.: HOL Light Real Analysis (2019). https:\/\/github.com\/jrh13\/hol-light\/tree\/master\/Multivariate\/realanalysis.ml","key":"9549_CR21"},{"issue":"2104","key":"9549_CR22","first-page":"20150399","volume":"375","author":"JW Hunt","year":"2017","unstructured":"Hunt, J.W., Kaufmann, M., Moore, J.S., Slobodova, A.: Industrial hardware and software verification with ACL2. Philos. Trans. 375(2104), 20150399 (2017)","journal-title":"Philos. Trans."},{"key":"9549_CR23","volume-title":"Calculus of Variations","author":"J Jost","year":"1998","unstructured":"Jost, J., Li-Jost, X.: Calculus of Variations. Cambridge University, Cambridge (1998)"},{"key":"9549_CR24","volume-title":"Modeling and Verification of Component Connectors in Coq","author":"Y Li","year":"2015","unstructured":"Li, Y., Sun, M.: Modeling and Verification of Component Connectors in Coq, vol. 113. Elsevier North-Holland Inc., New York (2015)"},{"issue":"4","key":"9549_CR25","doi-asserted-by":"publisher","first-page":"1305","DOI":"10.1007\/s00006-016-0650-5","volume":"26","author":"S Ma","year":"2016","unstructured":"Ma, S., Shi, Z., Shao, Z., Guan, Y., Li, L., Li, Y.: Higher-order logic formalization of conformal geometric algebra and its application in verifying a robotic manipulation algorithm. Adv. Appl. Clifford Algebras 26(4), 1305\u20131330 (2016)","journal-title":"Adv. Appl. Clifford Algebras"},{"issue":"12","key":"9549_CR26","first-page":"1","volume":"60","author":"M Maggesi","year":"2017","unstructured":"Maggesi, M.: A formalization of metric spaces in HOL Light. J. Autom. Reason. 60(12), 1\u201318 (2017)","journal-title":"J. Autom. Reason."},{"issue":"3","key":"9549_CR27","first-page":"209","volume":"38","author":"W Oberkampf","year":"2007","unstructured":"Oberkampf, W., Trucano, T.: Verification and validation in computational fluid dynamics. Adv. Mech. 38(3), 209\u2013272 (2007)","journal-title":"Adv. Mech."},{"unstructured":"Risteska, A., Kokalanov, V., Gicev, V.: Application of fundamental lemma of variational calculus to the Bernoulli\u2019s problem for the shortest time. In: Conference of Information Technology and Development of Education - ITRO 2015, pp. 159\u2013164 (2015). http:\/\/www.tfzr.uns.ac.rs\/itro\/Zbornik%20ITRO%202015.pdf","key":"9549_CR28"},{"unstructured":"Rumyantsev, V.: Lagrange equations (in mechanics). Encycl. Math. (2011)","key":"9549_CR29"},{"issue":"1\u20132","key":"9549_CR30","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BF02559565","volume":"102","author":"J Serrin","year":"1959","unstructured":"Serrin, J.: On a fundamental theorem of the calculus of variations. Acta Math. 102(1\u20132), 1\u201322 (1959)","journal-title":"Acta Math."},{"issue":"6","key":"9549_CR31","doi-asserted-by":"publisher","first-page":"739","DOI":"10.1007\/s00165-018-0468-0","volume":"30","author":"Z Shi","year":"2018","unstructured":"Shi, Z., Wu, A., Yang, X., Guan, Y., Li, Y., Song, X.: Formal analysis of the kinematic Jacobian in screw theory. Form. Asp. Comput. 30(6), 739\u2013757 (2018)","journal-title":"Form. Asp. Comput."},{"unstructured":"Slind, K., Norrish, M.: A brief overview of HOL4. In: Theorem Proving in Higher Order Logics, International Conference, Tphols 2008, Montreal, Canada, August 18\u201321, 2008. Proceedings, pp. 28\u201332 (2008)","key":"9549_CR32"},{"issue":"2","key":"9549_CR33","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/s10817-012-9269-y","volume":"50","author":"J Urban","year":"2013","unstructured":"Urban, J., Rudnicki, P., Sutcliffe, G.: ATP and presentation service for Mizar formalizations. J. Autom. Reason. 50(2), 229\u2013241 (2013)","journal-title":"J. Autom. Reason."},{"key":"9549_CR34","doi-asserted-by":"publisher","first-page":"270","DOI":"10.1007\/978-3-030-02450-5_16","volume-title":"Formal Methods and Software Engineering","author":"G Wang","year":"2018","unstructured":"Wang, G., Guan, Y., Shi, Z., Zhang, Q., Li, X., Li, Y.: Formalization of symplectic geometry in HOL-Light. In: Sun, J., Sun, M. (eds.) Formal Methods and Software Engineering, pp. 270\u2013283. Springer International Publishing, Cham (2018)"},{"key":"9549_CR35","first-page":"726","volume":"37","author":"X Yang","year":"2016","unstructured":"Yang, X., Shi, Z., Wu, A., Guan, Y., Ye, S., Zhang, J.: High order logic formalization for Jacobian matrix of a serial robot. J. Chin. Comput. Syst. 37, 726\u2013731 (2016)","journal-title":"J. Chin. Comput. Syst."},{"key":"9549_CR36","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1016\/j.jlamp.2019.04.004","volume":"106","author":"J Zhang","year":"2019","unstructured":"Zhang, J., Wang, G., Shi, Z., Guan, Y., Li, Y.: Formalization of functional variation in HOL Light. J. Log. Algebraic Methods Program. 106, 29\u201338 (2019)","journal-title":"J. Log. Algebraic Methods Program."},{"key":"9549_CR37","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1016\/j.tcs.2017.08.011","volume":"706","author":"C Zhao","year":"2017","unstructured":"Zhao, C., Li, S.: Formalization of fractional order PD control systems in HOL4. Theor. Comput. Sci. 706, 22\u201334 (2017)","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"9549_CR38","first-page":"22","volume":"706","author":"CN Zhao","year":"2017","unstructured":"Zhao, C.N., Li, S.S.: Formalization of fractional order PD control systems in HOL4. Theor. Comput. Sci. 706(1), 22\u201334 (2017)","journal-title":"Theor. Comput. Sci."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-020-09549-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-020-09549-w\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-020-09549-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,3,6]],"date-time":"2021-03-06T00:10:34Z","timestamp":1614989434000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-020-09549-w"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,3,6]]},"references-count":38,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2021,1]]}},"alternative-id":["9549"],"URL":"https:\/\/doi.org\/10.1007\/s10817-020-09549-w","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2020,3,6]]},"assertion":[{"value":"2 March 2019","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"23 February 2020","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"6 March 2020","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}