{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,26]],"date-time":"2026-09-26T23:39:38Z","timestamp":1790465978062,"version":"4.1.0"},"reference-count":17,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2018,11,9]],"date-time":"2018-11-09T00:00:00Z","timestamp":1541721600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100000943","name":"Commonwealth Scientific and Industrial Research Organisation","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100000943","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":[[2019,10]]},"DOI":"10.1007\/s10817-018-9495-z","type":"journal-article","created":{"date-parts":[[2018,11,9]],"date-time":"2018-11-09T03:16:20Z","timestamp":1541733380000},"page":"763-786","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["An Isabelle\/HOL Formalisation of Green\u2019s Theorem"],"prefix":"10.1007","volume":"63","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8244-518X","authenticated-orcid":false,"given":"Mohammad","family":"Abdulaziz","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Lawrence C.","family":"Paulson","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2018,11,9]]},"reference":[{"key":"9495_CR1","doi-asserted-by":"crossref","unstructured":"Abdulaziz, M., Paulson, L.C.: An Isabelle\/HOL formalisation of Green\u2019s theorem. In: Blanchette, J.C., Merz, S. (eds.) Interactive Theorem Proving\u20147th International Conference, ITP 2016. pp. 3\u201319. Springer (2016)","DOI":"10.1007\/978-3-319-43144-4_1"},{"key":"9495_CR2","volume-title":"Calculus","author":"TM Apostol","year":"1969","unstructured":"Apostol, T.M.: Calculus, vol. 2, 2nd edn. Wiley, New York (1969)","edition":"2"},{"key":"9495_CR3","volume-title":"Geometric Measure Theory","author":"H Federer","year":"2014","unstructured":"Federer, H.: Geometric Measure Theory. Springer, Berlin (2014)"},{"key":"9495_CR4","unstructured":"Green, G.: An essay on the application of mathematical analysis to the theories of electricity and magnetism. (1828) \n                    arXiv:0807.0088"},{"issue":"23","key":"9495_CR5","first-page":"151","volume":"10","author":"J Harrison","year":"2007","unstructured":"Harrison, J.: Formalizing basic complex analysis. From Insight to Proof: Festschrift in Honour of Andrzej Trybulec. Stud. Logic Gramm. Rhetor. 10(23), 151\u2013165 (2007)","journal-title":"Stud. Logic Gramm. Rhetor."},{"issue":"2","key":"9495_CR6","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."},{"key":"9495_CR7","doi-asserted-by":"crossref","unstructured":"H\u00f6lzl, J., Heller, A.: Three chapters of measure theory in Isabelle\/HOL. In: Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) Interactive Theorem Proving\u2014Second International Conference, pp. 135\u2013151. Springer (2011)","DOI":"10.1007\/978-3-642-22863-6_12"},{"key":"9495_CR8","doi-asserted-by":"crossref","unstructured":"H\u00f6lzl, J., Immler, F., Huffman, B.: Type classes and filters for mathematical analysis in Isabelle\/HOL. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) Interactive Theorem Proving\u20144th International Conference, pp. 279\u2013294. Springer (2013)","DOI":"10.1007\/978-3-642-39634-2_21"},{"issue":"4","key":"9495_CR9","first-page":"1003","volume":"109","author":"W Jurkat","year":"1990","unstructured":"Jurkat, W., Nonnenmacher, D.: The general form of Green\u2019s theorem. Proc. Am. Math. Soc. 109(4), 1003\u20131009 (1990)","journal-title":"Proc. Am. Math. Soc."},{"issue":"1","key":"9495_CR10","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1112\/jlms\/s1-30.1.1","volume":"1","author":"J Michael","year":"1955","unstructured":"Michael, J.: An approximation to a rectifiable plane curve. J. Lond. Math. Soc. 1(1), 1\u201311 (1955)","journal-title":"J. Lond. Math. Soc."},{"key":"9495_CR11","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: a proof assistant for higher-order logic. Springer, Berlin (2002)","DOI":"10.1007\/3-540-45949-9"},{"key":"9495_CR12","volume-title":"Basic Elements of Real Analysis","author":"MH Protter","year":"2006","unstructured":"Protter, M.H.: Basic Elements of Real Analysis. Springer, Berlin (2006)"},{"key":"9495_CR13","doi-asserted-by":"publisher","DOI":"10.1201\/9781315273747","volume-title":"Geometry of Curves","author":"JW Rutter","year":"2000","unstructured":"Rutter, J.W.: Geometry of Curves. CRC press, Boca Raton (2000)"},{"key":"9495_CR14","volume-title":"A Comprehensive Introduction to Differential Geometry","author":"M Spivak","year":"1981","unstructured":"Spivak, M.: A Comprehensive Introduction to Differential Geometry. Publish or Perish Inc., University of Tokyo Press (1981)"},{"key":"9495_CR15","doi-asserted-by":"publisher","DOI":"10.1142\/4361","volume-title":"Introduction to Gauge Integrals","author":"C Swartz","year":"2001","unstructured":"Swartz, C.: Introduction to Gauge Integrals. World Scientific, Singapore (2001)"},{"key":"9495_CR16","doi-asserted-by":"crossref","unstructured":"Wenzel, M.: Type classes and overloading in higher-order logic. In: Theorem Proving in Higher Order Logics, 10th International Conference, TPHOLs\u201997, Murray Hill, NJ, USA, August 19\u201322, 1997, Proceedings, pp. 307\u2013322 (1997)","DOI":"10.1007\/BFb0028402"},{"key":"9495_CR17","volume-title":"Mathematical Analysis II","author":"VA Zorich","year":"2004","unstructured":"Zorich, V.A., Cooke, R.: Mathematical Analysis II. Springer, Berlin (2004)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-018-9495-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-018-9495-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-018-9495-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,11,8]],"date-time":"2019-11-08T19:28:40Z","timestamp":1573241320000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-018-9495-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,11,9]]},"references-count":17,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2019,10]]}},"alternative-id":["9495"],"URL":"https:\/\/doi.org\/10.1007\/s10817-018-9495-z","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,11,9]]},"assertion":[{"value":"13 April 2017","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"31 October 2018","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"9 November 2018","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}