{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T10:42:11Z","timestamp":1740134531343,"version":"3.37.3"},"reference-count":9,"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":[{"DOI":"10.13039\/501100012166","name":"National Basic Research Program of China","doi-asserted-by":"crossref","award":["2010CB328000","U1201251","61133016","2012AA040906","2013GXNSFAA019342","2012Q017"],"award-info":[{"award-number":["2010CB328000","U1201251","61133016","2012AA040906","2013GXNSFAA019342","2012Q017"]}],"id":[{"id":"10.13039\/501100012166","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["2010CB328000","U1201251","61133016","2012AA040906","2013GXNSFAA019342","2012Q017"],"award-info":[{"award-number":["2010CB328000","U1201251","61133016","2012AA040906","2013GXNSFAA019342","2012Q017"]}],"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":["2010CB328000","U1201251","61133016","2012AA040906","2013GXNSFAA019342","2012Q017"],"award-info":[{"award-number":["2010CB328000","U1201251","61133016","2012AA040906","2013GXNSFAA019342","2012Q017"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"name":"National High-Tech Research and Development Program of China","award":["2010CB328000","U1201251","61133016","2012AA040906","2013GXNSFAA019342","2012Q017"],"award-info":[{"award-number":["2010CB328000","U1201251","61133016","2012AA040906","2013GXNSFAA019342","2012Q017"]}]},{"name":"National Natural Science Foundation of Guangxi","award":["2010CB328000","U1201251","61133016","2012AA040906","2013GXNSFAA019342","2012Q017"],"award-info":[{"award-number":["2010CB328000","U1201251","61133016","2012AA040906","2013GXNSFAA019342","2012Q017"]}]},{"name":"GUN Project","award":["2010CB328000","U1201251","61133016","2012AA040906","2013GXNSFAA019342","2012Q017"],"award-info":[{"award-number":["2010CB328000","U1201251","61133016","2012AA040906","2013GXNSFAA019342","2012Q017"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Applied Mathematics"],"published-print":{"date-parts":[[2014]]},"abstract":"<jats:p>The paper presents a formal proof of a machine closed theorem of TLA<jats:sup>+<\/jats:sup>in the theorem proving system Coq. A shallow embedding scheme is employed for the proof which is independent of concrete syntax. Fundamental concepts need to state that the machine closed theorems are addressed in the proof platform. A useful proof pattern of constructing a trace with desired properties is devised. A number of Coq reusable libraries are established.<\/jats:p>","DOI":"10.1155\/2014\/892832","type":"journal-article","created":{"date-parts":[[2014,3,30]],"date-time":"2014-03-30T21:06:05Z","timestamp":1396213565000},"page":"1-9","source":"Crossref","is-referenced-by-count":0,"title":["Formal Proof of a Machine Closed Theorem in Coq"],"prefix":"10.1155","volume":"2014","author":[{"given":"Hai","family":"Wan","sequence":"first","affiliation":[{"name":"School of Software, Tsinghua University, NLIST, KLISS, Beijing 100084, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anping","family":"He","sequence":"additional","affiliation":[{"name":"Guangxi Key Laboratory of Hybrid Computation and IC Design Analysis, Guangxi University for Nationalities, Nanning, Guangxi 530006, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhiyang","family":"You","sequence":"additional","affiliation":[{"name":"General office of the Guangxi Zhuang Autonomous Region People\u2019s Government, Nanning, Guangxi 530003, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xibin","family":"Zhao","sequence":"additional","affiliation":[{"name":"School of Software, Tsinghua University, NLIST, KLISS, Beijing 100084, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"311","reference":[{"key":"2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74107-7_8"},{"key":"3","doi-asserted-by":"publisher","DOI":"10.1145\/177492.177726"},{"key":"4","doi-asserted-by":"publisher","DOI":"10.1145\/186025.186058"},{"key":"6","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(91)90224-P"},{"key":"7","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/13.6.801"},{"first-page":"xxvi+469","year":"2004","series-title":"Coq'Art: The Calculus of Inductive Constructions","key":"8"},{"first-page":"1","volume-title":"Combining model checking and deduction for I\/O-automata","year":"1995","key":"10"},{"key":"11","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0030627"},{"first-page":"316","volume-title":"Formalization of CTL* in calculus of inductive constructions","year":"2006","key":"12"}],"container-title":["Journal of Applied Mathematics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/downloads.hindawi.com\/journals\/jam\/2014\/892832.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/downloads.hindawi.com\/journals\/jam\/2014\/892832.xml","content-type":"application\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/downloads.hindawi.com\/journals\/jam\/2014\/892832.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,11]],"date-time":"2020-05-11T21:34:03Z","timestamp":1589232843000},"score":1,"resource":{"primary":{"URL":"http:\/\/www.hindawi.com\/journals\/jam\/2014\/892832\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"references-count":9,"alternative-id":["892832","892832"],"URL":"https:\/\/doi.org\/10.1155\/2014\/892832","relation":{},"ISSN":["1110-757X","1687-0042"],"issn-type":[{"type":"print","value":"1110-757X"},{"type":"electronic","value":"1687-0042"}],"subject":[],"published":{"date-parts":[[2014]]}}}