{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,28]],"date-time":"2025-05-28T06:25:30Z","timestamp":1748413530945},"reference-count":20,"publisher":"Cambridge University Press (CUP)","issue":"4","license":[{"start":{"date-parts":[[2011,7,1]],"date-time":"2011-07-01T00:00:00Z","timestamp":1309478400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2011,8]]},"abstract":"<jats:p>Pick's Theorem relates the area of a simple polygon with vertices at integer lattice points to the number of lattice points in its inside and boundary. We describe a formal proof of this theorem using the HOL Light theorem prover. As sometimes happens for highly geometrical proofs, the formalisation turned out to be more work than initially expected. The difficulties arose mostly from formalising the triangulation process for an arbitrary polygon.<\/jats:p>","DOI":"10.1017\/s0960129511000089","type":"journal-article","created":{"date-parts":[[2011,7,1]],"date-time":"2011-07-01T10:53:35Z","timestamp":1309517615000},"page":"715-729","source":"Crossref","is-referenced-by-count":2,"title":["A formal proof of Pick's Theorem"],"prefix":"10.1017","volume":"21","author":[{"given":"JOHN","family":"HARRISON","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2011,7,1]]},"reference":[{"key":"S0960129511000089_ref5","first-page":"25","article-title":"Sur un probl\u00e8me de g\u00e9om\u00e9trie diophantienne lin\u00e9aire II.","volume":"227","author":"Ehrhart","year":"1967","journal-title":"Journal f\u00fcr die reine und angewandte Mathematik"},{"key":"S0960129511000089_ref3","first-page":"431","article-title":"Pick's formula via the Weierstrass -function.","volume":"102","author":"Diaz","year":"1995","journal-title":"The American Mathematical Monthly"},{"key":"S0960129511000089_ref11","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9145-6"},{"key":"S0960129511000089_ref1","doi-asserted-by":"publisher","DOI":"10.1090\/gsm\/054"},{"key":"S0960129511000089_ref2","doi-asserted-by":"publisher","DOI":"10.1080\/0025570X.1997.11996531"},{"key":"S0960129511000089_ref17","first-page":"311","article-title":"Geometrisches zur Zahlenlehre.","volume":"19","author":"Pick","year":"1899","journal-title":"Sitzungsberichte des Deutschen Naturwissenschaftlich-Medicinischen Vereines f\u00fcr B\u00f6hmen \u2018Lotos\u2019 in Prag, Series 2"},{"key":"S0960129511000089_ref20","doi-asserted-by":"publisher","DOI":"10.1515\/9781400879335"},{"key":"S0960129511000089_ref10","first-page":"63","article-title":"A formalized proof of Dirichlet's theorem on primes in arithmetic progression","volume":"2","author":"Harrison","year":"2009","journal-title":"Journal of Formalized Reasoning"},{"key":"S0960129511000089_ref8","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0031814"},{"key":"S0960129511000089_ref14","doi-asserted-by":"publisher","DOI":"10.2307\/2369986"},{"key":"S0960129511000089_ref15","doi-asserted-by":"publisher","DOI":"10.1080\/00029890.2007.11920465"},{"key":"S0960129511000089_ref9","first-page":"114","volume-title":"Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005","author":"Harrison","year":"2005"},{"key":"S0960129511000089_ref12","first-page":"43","volume-title":"Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2009","author":"Harrison","year":"2009"},{"key":"S0960129511000089_ref13","first-page":"723","article-title":"From Homma's theorem to Pick's theorem.","volume":"42","author":"Kurogi","year":"2005","journal-title":"Osaka Journal of Mathematics"},{"key":"S0960129511000089_ref19","volume-title":"Convexity","author":"Webster","year":"1995"},{"key":"S0960129511000089_ref16","volume-title":"Elements of the Topology of Plane Sets of Points","author":"Newman","year":"1939"},{"key":"S0960129511000089_ref6","unstructured":"Hales T. C. (2007a). Easy pieces in geometry. (Available at http:\/\/www.math.pitt.edu\/~thales\/papers\/.)"},{"key":"S0960129511000089_ref7","doi-asserted-by":"publisher","DOI":"10.1080\/00029890.2007.11920481"},{"key":"S0960129511000089_ref18","first-page":"116","article-title":"The Jordan-Schoenflies theorem and the classification of surfaces.","volume":"99","author":"Thomassen","year":"1992","journal-title":"The American Mathematical Monthly"},{"key":"S0960129511000089_ref4","doi-asserted-by":"publisher","DOI":"10.12988\/ijcms.2007.07094"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129511000089","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,27]],"date-time":"2019-04-27T03:26:50Z","timestamp":1556335610000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129511000089\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,7,1]]},"references-count":20,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2011,8]]}},"alternative-id":["S0960129511000089"],"URL":"https:\/\/doi.org\/10.1017\/s0960129511000089","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,7,1]]}}}