{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T10:42:38Z","timestamp":1740134558863,"version":"3.37.3"},"reference-count":7,"publisher":"Wiley","license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/3.0\/"}],"funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["60873006","61070049","61170304","61104035","2010DFB10930","2011DFG13000","4122017","KZ201210028036"],"award-info":[{"award-number":["60873006","61070049","61170304","61104035","2010DFB10930","2011DFG13000","4122017","KZ201210028036"]}],"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":["60873006","61070049","61170304","61104035","2010DFB10930","2011DFG13000","4122017","KZ201210028036"],"award-info":[{"award-number":["60873006","61070049","61170304","61104035","2010DFB10930","2011DFG13000","4122017","KZ201210028036"]}],"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":["60873006","61070049","61170304","61104035","2010DFB10930","2011DFG13000","4122017","KZ201210028036"],"award-info":[{"award-number":["60873006","61070049","61170304","61104035","2010DFB10930","2011DFG13000","4122017","KZ201210028036"]}],"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":["60873006","61070049","61170304","61104035","2010DFB10930","2011DFG13000","4122017","KZ201210028036"],"award-info":[{"award-number":["60873006","61070049","61170304","61104035","2010DFB10930","2011DFG13000","4122017","KZ201210028036"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"name":"International Cooperation Program on Science and Technology","award":["60873006","61070049","61170304","61104035","2010DFB10930","2011DFG13000","4122017","KZ201210028036"],"award-info":[{"award-number":["60873006","61070049","61170304","61104035","2010DFB10930","2011DFG13000","4122017","KZ201210028036"]}]},{"name":"International Cooperation Program on Science and Technology","award":["60873006","61070049","61170304","61104035","2010DFB10930","2011DFG13000","4122017","KZ201210028036"],"award-info":[{"award-number":["60873006","61070049","61170304","61104035","2010DFB10930","2011DFG13000","4122017","KZ201210028036"]}]},{"DOI":"10.13039\/501100004826","name":"Natural Science Foundation of Beijing Municipality","doi-asserted-by":"publisher","award":["60873006","61070049","61170304","61104035","2010DFB10930","2011DFG13000","4122017","KZ201210028036"],"award-info":[{"award-number":["60873006","61070049","61170304","61104035","2010DFB10930","2011DFG13000","4122017","KZ201210028036"]}],"id":[{"id":"10.13039\/501100004826","id-type":"DOI","asserted-by":"publisher"}]},{"name":"S&R Key Program of the Beijing Municipal Education Commission","award":["60873006","61070049","61170304","61104035","2010DFB10930","2011DFG13000","4122017","KZ201210028036"],"award-info":[{"award-number":["60873006","61070049","61170304","61104035","2010DFB10930","2011DFG13000","4122017","KZ201210028036"]}]},{"name":"Open Project Program of State Key Laboratory of Computer Architecture","award":["60873006","61070049","61170304","61104035","2010DFB10930","2011DFG13000","4122017","KZ201210028036"],"award-info":[{"award-number":["60873006","61070049","61170304","61104035","2010DFB10930","2011DFG13000","4122017","KZ201210028036"]}]},{"name":"Open Project Program of Guangxi Key Laboratory of Trusted Software","award":["60873006","61070049","61170304","61104035","2010DFB10930","2011DFG13000","4122017","KZ201210028036"],"award-info":[{"award-number":["60873006","61070049","61170304","61104035","2010DFB10930","2011DFG13000","4122017","KZ201210028036"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Applied Mathematics"],"published-print":{"date-parts":[[2013]]},"abstract":"<jats:p>The integral is one of the most important foundations for modeling dynamical systems. The gauge integral is a generalization of the Riemann integral and the Lebesgue integral and applies to a much wider class of functions. In this paper, we formalize the operational properties which contain the linearity, monotonicity, integration by parts, the Cauchy-type integrability criterion, and other important theorems of the gauge integral in higher-order logic 4 (HOL4) and then use them to verify an inverting integrator. The formalized theorem library has been accepted by the HOL4 authority and will appear in HOL4 Kananaskis-9.<\/jats:p>","DOI":"10.1155\/2013\/160875","type":"journal-article","created":{"date-parts":[[2013,5,3]],"date-time":"2013-05-03T02:16:40Z","timestamp":1367547400000},"page":"1-7","source":"Crossref","is-referenced-by-count":3,"title":["The Gauge Integral Theory in HOL4"],"prefix":"10.1155","volume":"2013","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6401-5506","authenticated-orcid":true,"given":"Zhiping","family":"Shi","sequence":"first","affiliation":[{"name":"Beijing Engineering Research Center of High Reliable Embedded System, Capital Normal University, Beijing 100048, China"},{"name":"State Key Laboratory of Computer Architecture, Institute of Computing Technology, Chinese Academy of Sciences, Beijing 100190, China"}]},{"given":"Weiqing","family":"Gu","sequence":"additional","affiliation":[{"name":"Beijing Engineering Research Center of High Reliable Embedded System, Capital Normal University, Beijing 100048, China"}]},{"given":"Xiaojuan","family":"Li","sequence":"additional","affiliation":[{"name":"Beijing Engineering Research Center of High Reliable Embedded System, Capital Normal University, Beijing 100048, China"}]},{"given":"Yong","family":"Guan","sequence":"additional","affiliation":[{"name":"Beijing Engineering Research Center of High Reliable Embedded System, Capital Normal University, Beijing 100048, China"}]},{"given":"Shiwei","family":"Ye","sequence":"additional","affiliation":[{"name":"College of Information Science and Engineering, Graduate University of Chinese Academy of Sciences, Beijing 100049, China"}]},{"given":"Jie","family":"Zhang","sequence":"additional","affiliation":[{"name":"College of Information Science and Technology, Beijing University of Chemical Technology, Beijing 100029, China"}]},{"given":"Hongxing","family":"Wei","sequence":"additional","affiliation":[{"name":"School of Mechanical Engineering and Automation, Beijing University of Aeronautics and Astronautics, Beijing 100191, China"}]}],"member":"311","reference":[{"issue":"2","key":"1","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1145\/307988.307989","volume":"4","year":"1999","journal-title":"ACM Transactions on Design Automation of Electronic Systems"},{"key":"3","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44659-1_10"},{"issue":"1","key":"5","first-page":"1","volume":"2","year":"2009","journal-title":"Journal of Formalized Reasoning"},{"key":"6","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14052-5_27"},{"key":"7","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-1591-5"},{"key":"8","doi-asserted-by":"publisher","DOI":"10.1142\/9789812810656"},{"key":"9","series-title":"Graduate Studies in Mathematics","first-page":"xii+395","volume":"4","year":"1994"}],"container-title":["Journal of Applied Mathematics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/downloads.hindawi.com\/journals\/jam\/2013\/160875.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/downloads.hindawi.com\/journals\/jam\/2013\/160875.xml","content-type":"application\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/downloads.hindawi.com\/journals\/jam\/2013\/160875.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,21]],"date-time":"2017-06-21T08:27:51Z","timestamp":1498033671000},"score":1,"resource":{"primary":{"URL":"http:\/\/www.hindawi.com\/journals\/jam\/2013\/160875\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"references-count":7,"alternative-id":["160875","160875"],"URL":"https:\/\/doi.org\/10.1155\/2013\/160875","relation":{},"ISSN":["1110-757X","1687-0042"],"issn-type":[{"type":"print","value":"1110-757X"},{"type":"electronic","value":"1687-0042"}],"subject":[],"published":{"date-parts":[[2013]]}}}