{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T10:42:45Z","timestamp":1740134565281,"version":"3.37.3"},"reference-count":12,"publisher":"Wiley","license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/3.0\/"}],"funder":[{"name":"International Cooperation Program on Science and Technology","award":["2010DFB10930","2011DFG13000","61070049","61170304","61104035","61373034","61303014","4122017","KZ201210028036"],"award-info":[{"award-number":["2010DFB10930","2011DFG13000","61070049","61170304","61104035","61373034","61303014","4122017","KZ201210028036"]}]},{"name":"International Cooperation Program on Science and Technology","award":["2010DFB10930","2011DFG13000","61070049","61170304","61104035","61373034","61303014","4122017","KZ201210028036"],"award-info":[{"award-number":["2010DFB10930","2011DFG13000","61070049","61170304","61104035","61373034","61303014","4122017","KZ201210028036"]}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["2010DFB10930","2011DFG13000","61070049","61170304","61104035","61373034","61303014","4122017","KZ201210028036"],"award-info":[{"award-number":["2010DFB10930","2011DFG13000","61070049","61170304","61104035","61373034","61303014","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":["2010DFB10930","2011DFG13000","61070049","61170304","61104035","61373034","61303014","4122017","KZ201210028036"],"award-info":[{"award-number":["2010DFB10930","2011DFG13000","61070049","61170304","61104035","61373034","61303014","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":["2010DFB10930","2011DFG13000","61070049","61170304","61104035","61373034","61303014","4122017","KZ201210028036"],"award-info":[{"award-number":["2010DFB10930","2011DFG13000","61070049","61170304","61104035","61373034","61303014","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":["2010DFB10930","2011DFG13000","61070049","61170304","61104035","61373034","61303014","4122017","KZ201210028036"],"award-info":[{"award-number":["2010DFB10930","2011DFG13000","61070049","61170304","61104035","61373034","61303014","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":["2010DFB10930","2011DFG13000","61070049","61170304","61104035","61373034","61303014","4122017","KZ201210028036"],"award-info":[{"award-number":["2010DFB10930","2011DFG13000","61070049","61170304","61104035","61373034","61303014","4122017","KZ201210028036"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100004826","name":"Natural Science Foundation of Beijing Municipality","doi-asserted-by":"publisher","award":["2010DFB10930","2011DFG13000","61070049","61170304","61104035","61373034","61303014","4122017","KZ201210028036"],"award-info":[{"award-number":["2010DFB10930","2011DFG13000","61070049","61170304","61104035","61373034","61303014","4122017","KZ201210028036"]}],"id":[{"id":"10.13039\/501100004826","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100003213","name":"Beijing Municipal Education Commission","doi-asserted-by":"publisher","award":["2010DFB10930","2011DFG13000","61070049","61170304","61104035","61373034","61303014","4122017","KZ201210028036"],"award-info":[{"award-number":["2010DFB10930","2011DFG13000","61070049","61170304","61104035","61373034","61303014","4122017","KZ201210028036"]}],"id":[{"id":"10.13039\/501100003213","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Applied Mathematics"],"published-print":{"date-parts":[[2014]]},"abstract":"<jats:p>Function matrices, in which elements are functions rather than numbers, are widely used in model analysis of dynamic systems such as control systems and robotics. In safety-critical applications, the dynamic systems are required to be analyzed formally and accurately to ensure their correctness and safeness. Higher-order logic (HOL) theorem proving is a promise technique to match the requirement. This paper proposes a higher-order logic formalization of the function vector and the function matrix theories using the HOL theorem prover, including data types, operations, and their properties, and further presents formalization of the differential and integral of function vectors and function matrices. The formalization is implemented as a library in the HOL system. A case study, a formal analysis of differential of quadratic functions, is presented to show the usefulness of the proposed formalization.<\/jats:p>","DOI":"10.1155\/2014\/201214","type":"journal-article","created":{"date-parts":[[2014,7,24]],"date-time":"2014-07-24T17:56:26Z","timestamp":1406224586000},"page":"1-10","source":"Crossref","is-referenced-by-count":5,"title":["Formalization of Function Matrix Theory in HOL"],"prefix":"10.1155","volume":"2014","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6401-5506","authenticated-orcid":true,"given":"Zhiping","family":"Shi","sequence":"first","affiliation":[{"name":"Beijing Key Laboratory of Electronic System Reliability Technology, Capital Normal University, Beijing 100048, China"},{"name":"Guangxi Key Laboratory of Trusted Software, Guilin University of Electronic Technology, Guilin 541004, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhenke","family":"Liu","sequence":"additional","affiliation":[{"name":"Beijing Key Laboratory of Electronic System Reliability Technology, Capital Normal University, Beijing 100048, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yong","family":"Guan","sequence":"additional","affiliation":[{"name":"Beijing Key Laboratory of Electronic System Reliability Technology, Capital Normal University, Beijing 100048, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shiwei","family":"Ye","sequence":"additional","affiliation":[{"name":"College of Information Science and Engineering, Graduate University of Chinese Academy of Sciences, Beijing 100049, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jie","family":"Zhang","sequence":"additional","affiliation":[{"name":"College of Information Science and Technology, Beijing University of Chemical Technology, Beijing 100029, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hongxing","family":"Wei","sequence":"additional","affiliation":[{"name":"School of Mechanical Engineering and Automation, Beijing University of Aeronautics and Astronautics, Beijing 100191, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"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":"2","doi-asserted-by":"publisher","DOI":"10.1007\/s11704-007-0001-8"},{"key":"3","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15240-5_17"},{"key":"4","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2011.01.032"},{"key":"5","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-010-9210-1"},{"issue":"1","key":"6","first-page":"21","volume":"14","year":"2006","journal-title":"Formalized Mathematics"},{"key":"7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14128-7_19"},{"key":"8","doi-asserted-by":"publisher","DOI":"10.1007\/11541868_8"},{"key":"9","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9"},{"key":"11","doi-asserted-by":"publisher","DOI":"10.1007\/11541868_15"},{"key":"12","doi-asserted-by":"publisher","DOI":"10.1155\/2013\/160875"},{"year":"2007","key":"13"}],"container-title":["Journal of Applied Mathematics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/downloads.hindawi.com\/journals\/jam\/2014\/201214.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/downloads.hindawi.com\/journals\/jam\/2014\/201214.xml","content-type":"application\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/downloads.hindawi.com\/journals\/jam\/2014\/201214.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,22]],"date-time":"2017-06-22T13:16:57Z","timestamp":1498137417000},"score":1,"resource":{"primary":{"URL":"http:\/\/www.hindawi.com\/journals\/jam\/2014\/201214\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"references-count":12,"alternative-id":["201214","201214"],"URL":"https:\/\/doi.org\/10.1155\/2014\/201214","relation":{},"ISSN":["1110-757X","1687-0042"],"issn-type":[{"type":"print","value":"1110-757X"},{"type":"electronic","value":"1687-0042"}],"subject":[],"published":{"date-parts":[[2014]]}}}