{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,20]],"date-time":"2026-04-20T12:52:37Z","timestamp":1776689557801,"version":"3.51.2"},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540371878","type":"print"},{"value":"9783540371885","type":"electronic"}],"license":[{"start":{"date-parts":[[2006,1,1]],"date-time":"2006-01-01T00:00:00Z","timestamp":1136073600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11814771_4","type":"book-chapter","created":{"date-parts":[[2006,10,5]],"date-time":"2006-10-05T11:44:21Z","timestamp":1160048661000},"page":"21-35","source":"Crossref","is-referenced-by-count":29,"title":["Flyspeck I: Tame Graphs"],"prefix":"10.1007","author":[{"given":"Tobias","family":"Nipkow","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gertrud","family":"Bauer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Paula","family":"Schultz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"4_CR1","unstructured":"Bauer, G.: Formalizing Plane Graph Theory \u2014 Towards a Formalized Proof of the Kepler Conjecture. PhD thesis, Technische Universit\u00e4t M\u00fcnchen (2006)"},{"key":"4_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/3-540-45842-5_2","volume-title":"Types for Proofs and Programs","author":"S. Berghofer","year":"2002","unstructured":"Berghofer, S., Nipkow, T.: Executing higher order logic. In: Callaghan, P., Luo, Z., McKinna, J., Pollack, R. (eds.) TYPES 2000. LNCS, vol.\u00a02277, pp. 24\u201340. Springer, Heidelberg (2002)"},{"key":"4_CR3","unstructured":"Gonthier, G.: A computer-checked proof of the four colour theorem, available at \n                    \n                      research.microsoft.com\/~gonthier\/4colproof.pdf"},{"key":"4_CR4","first-page":"440","volume":"47","author":"T.C. Hales","year":"2000","unstructured":"Hales, T.C.: Cannonballs and honeycombs. Notices Amer. Math. Soc.\u00a047, 440\u2013449 (2000)","journal-title":"Notices Amer. Math. Soc."},{"key":"4_CR5","doi-asserted-by":"publisher","first-page":"1063","DOI":"10.4007\/annals.2005.162.1065","volume":"162","author":"T.C. Hales","year":"2005","unstructured":"Hales, T.C.: A proof of the Kepler conjecture. Annals of Mathematics\u00a0162, 1063\u20131183 (2005)","journal-title":"Annals of Mathematics"},{"key":"4_CR6","doi-asserted-by":"crossref","unstructured":"Hales, T.C.: Sphere packings, VI. Tame graphs and linear programs. Discrete and Computational Geometry (to appear, 2006)","DOI":"10.1007\/s00454-005-1215-x"},{"key":"4_CR7","unstructured":"Hales, T.C., McLaughlin, S.: A proof of the dodecahedral conjecture, E-print archive \n                    \n                      arXiv.org\/abs\/math.MG\/9811079"},{"key":"4_CR8","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1145\/800119.803896","volume-title":"STOC 1974: Proc. 6th ACM Symposium Theory of Computing","author":"J.E. Hopcroft","year":"1974","unstructured":"Hopcroft, J.E., Wong, J.K.: Linear time algorithm for isomorphism of planar graphs (preliminary report). In: STOC 1974: Proc. 6th ACM Symposium Theory of Computing, pp. 172\u2013184. ACM Press, New York (1974)"},{"key":"4_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L., Wenzel, M.: Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic. In: Nipkow, T., Paulson, L.C., Wenzel, M.T. (eds.) Isabelle\/HOL. LNCS, vol.\u00a02283, Springer, Heidelberg (2002), \n                    \n                      http:\/\/www.in.tum.de\/~nipkow\/LNCS2283\/"},{"key":"4_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1007\/11541868_15","volume-title":"Theorem Proving in Higher Order Logics","author":"S. Obua","year":"2005","unstructured":"S.\u00a0Obua. Proving bounds for real linear programs in Isabelle\/HOL. In J.\u00a0Hurd, editor, Theorem Proving in Higher Order Logics (TPHOLs 2005), volume 3603 of Lect. Notes in Comp. Sci., pages 227\u2013244. Springer-Verlag, 2005."},{"key":"4_CR11","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","DOI":"10.1007\/11814771_35","volume-title":"Automated Reasoning","author":"R. Zumkeller","year":"2006","unstructured":"Zumkeller, R.: A formalization of global optimization with Taylor models. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, Springer, Heidelberg (2006)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11814771_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T19:33:38Z","timestamp":1558294418000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11814771_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540371878","9783540371885"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/11814771_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006]]}}}