{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,3,17]],"date-time":"2024-03-17T14:10:58Z","timestamp":1710684658251},"reference-count":30,"publisher":"Springer Science and Business Media LLC","issue":"3-4","license":[{"start":{"date-parts":[[2009,8,1]],"date-time":"2009-08-01T00:00:00Z","timestamp":1249084800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Ann Math Artif Intell"],"published-print":{"date-parts":[[2009,8]]},"DOI":"10.1007\/s10472-009-9168-z","type":"journal-article","created":{"date-parts":[[2009,11,6]],"date-time":"2009-11-06T10:06:19Z","timestamp":1257501979000},"page":"245-272","source":"Crossref","is-referenced-by-count":7,"title":["Flyspeck II: the basic linear programs"],"prefix":"10.1007","volume":"56","author":[{"given":"Steven","family":"Obua","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tobias","family":"Nipkow","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2009,11,7]]},"reference":[{"key":"9168_CR1","series-title":"LNCS","first-page":"39","volume-title":"TPHOLs 2008","author":"K Aehlig","year":"2008","unstructured":"Aehlig, K., Haftmann, F., Nipkow, T.: A compiled implementation of normalization by evaluation. In: Mohamed, A., Munoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 39\u201354. Springer, New York (2008)"},{"key":"9168_CR2","series-title":"Lecture Notes in Computer Science","first-page":"34","volume-title":"TYPES","author":"C Ballarin","year":"2003","unstructured":"Ballarin, C.: Locales and locale expressions in Isabelle\/Isar. In: Berardi, S., Coppo, M., Damiani, F. (eds.) TYPES. Lecture Notes in Computer Science, vol. 3085, pp. 34\u201350. Springer, New York (2003)"},{"key":"9168_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"17","DOI":"10.1007\/3-540-44659-1_2","volume-title":"TPHOLs","author":"B Barras","year":"2000","unstructured":"Barras, B.: Programming and computing in HOL. In: Aagaard, M., Harrison, J. (eds.) TPHOLs. Lecture Notes in Computer Science, vol. 1869, pp. 17\u201337. Springer, New York (2000)"},{"key":"9168_CR4","unstructured":"Berghofer, S.: Proofs, programs and executable specifications in higher order logic. Ph.D. thesis, Technische Universit\u00e4t M\u00fcnchen (2003)"},{"key":"9168_CR5","volume-title":"Lattice Theory","author":"G Birkhoff","year":"1967","unstructured":"Birkhoff, G.: Lattice Theory. AMS, Providence (1967)"},{"key":"9168_CR6","volume-title":"A Computational Logic","author":"RS Boyer","year":"1979","unstructured":"Boyer, R.S., Moore, J.S.: A Computational Logic. Academic, New York (1979)"},{"key":"9168_CR7","unstructured":"The COQ development team: The COQ reference manual, version\u00a08.2. http:\/\/coq.inria.fr (2009)"},{"key":"9168_CR8","unstructured":"Gonthier, G.: A computer-checked proof of the four color theorem. http:\/\/research.microsoft.com\/~gonthier\/4colproof.pdf"},{"key":"9168_CR9","unstructured":"Gonthier, G.: Formal proof\u2014the four color theorem. Not. Am. Math. Soc. 55 (2008)"},{"key":"9168_CR10","doi-asserted-by":"crossref","first-page":"169","DOI":"10.7551\/mitpress\/5641.003.0012","volume-title":"Proof, Language, and Interaction: Essays in Honour of Robin Milner","author":"M Gordon","year":"2000","unstructured":"Gordon, M.: From LCF to HOL: a short history. In: Proof, Language, and Interaction: Essays in Honour of Robin Milner, pp. 169\u2013185. MIT, Cambridge (2000)"},{"issue":"3","key":"9168_CR11","doi-asserted-by":"crossref","first-page":"250","DOI":"10.1145\/355791.355796","volume":"4","author":"FG Gustavson","year":"1978","unstructured":"Gustavson, F.G.: Two fast algorithms for sparse matrices: multiplication and permuted transposition. ACM Trans. Math. Softw. 4(3), 250\u2013269 (1978)","journal-title":"ACM Trans. Math. Softw."},{"key":"9168_CR12","unstructured":"Haftmann, F.: Code generation from specifications in higher-order logic. Ph.D. thesis, Technische Universit\u00e4t M\u00fcnchen (2009)"},{"key":"9168_CR13","unstructured":"Hales, T.C.: Sphere packings III. arXiv:math\/9811075v2"},{"key":"9168_CR14","doi-asserted-by":"crossref","first-page":"1065","DOI":"10.4007\/annals.2005.162.1065","volume":"162","author":"TC Hales","year":"2005","unstructured":"Hales, T.C., Ferguson, S.P.: A proof of the Kepler conjecture. Ann. Math. 162, 1065\u20131185 (2005)","journal-title":"Ann. Math."},{"key":"9168_CR15","doi-asserted-by":"crossref","unstructured":"Hales, T.C., Ferguson, S.P.: The Kepler conjecture. Discrete Comput. Geom. 36, (2006)","DOI":"10.1007\/s00454-005-1211-1"},{"key":"9168_CR16","doi-asserted-by":"crossref","unstructured":"Hales, T.C., Harrison, J., McLaughlin, S., Nipkow, T., Obua, S., Zumkeller, R.: A revision of the proof of the Kepler Conjecture. Discrete Comput. Geom. (2009)","DOI":"10.1007\/s00454-009-9148-4"},{"key":"9168_CR17","series-title":"Lecture Notes in Computer Science","volume-title":"TPHOLs 2005","author":"J Harrison","year":"2005","unstructured":"Harrison, J.: A HOL theory of Euclidean space. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. Lecture Notes in Computer Science, vol. 3603. Springer, Oxford (2005)"},{"key":"9168_CR18","unstructured":"H\u00f6lzl, J.: Proving inequalities over reals with computation in Isabelle\/HOL. In: Proceedings of the ACM SIGSAM 2009 International Workshop on Programming Languages for Mechanized Mathematics Systems (PLMMS 2009) (2009)"},{"key":"9168_CR19","series-title":"Lecture Notes in Computer Science","first-page":"22","volume-title":"Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, Oxford, UK, 22\u201325 August 2005, Proceedings","year":"2005","unstructured":"Hurd, J., Melham, T.F. (eds.): Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, Oxford, UK, 22\u201325 August 2005, Proceedings. Lecture Notes in Computer Science, vol. 3603. Springer, New York (2005)"},{"key":"9168_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"589","DOI":"10.1007\/11814771_48","volume-title":"IJCAR","author":"A Krauss","year":"2006","unstructured":"Krauss, A.: Partial recursive functions in higher-order logic. In: Furbach, U., Shankar, N. (eds.) IJCAR. Lecture Notes in Computer Science, vol. 4130, pp. 589\u2013603. Springer, New York (2006)"},{"key":"9168_CR21","volume-title":"Algebra","author":"S Lang","year":"1974","unstructured":"Lang, S.: Algebra. Addison-Wesley, Reading (1974)"},{"key":"9168_CR22","unstructured":"Nipkow, T., Bauer, G., Schultz, P.: The archive of tame graphs. http:\/\/www4.informatik.tu-muenchen.de\/~nipkow\/pubs\/Flyspeck (2006)"},{"key":"9168_CR23","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Bauer, G., Schultz, P.: Flyspeck I: tame graphs. In: IJCAR, pp.\u00a021\u201335 (2006)","DOI":"10.1007\/11814771_4"},{"key":"9168_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"385","DOI":"10.1007\/11541868_25","volume-title":"Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, Oxford, UK, 22\u201325 August 2005, Proceedings","author":"T Nipkow","year":"2005","unstructured":"Nipkow, T., Paulson, L.C.: Proof pearl: defining functions over finite sets. In: Hurd, J., Melham, T.F. (eds.) Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, Oxford, UK, 22\u201325 August 2005, Proceedings. Lecture Notes in Computer Science, vol.\u00a03603, pp.\u00a0385\u2013396. Springer, New York (2005)"},{"key":"9168_CR25","volume-title":"Lecture Notes in Computer Science, vol.\u00a02283","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL\u2014a proof assistant for higher-order logic. In: Lecture Notes in Computer Science, vol.\u00a02283. Springer, New York (2002)"},{"key":"9168_CR26","unstructured":"Obua, S.: Flyspeck II: the basic linear programs. http:\/\/www4.in.tum.de\/~obua\/flyspeckII (2007)"},{"key":"9168_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"227","DOI":"10.1007\/11541868_15","volume-title":"Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, Oxford, UK, 22\u201325 August 2005, Proceedings","author":"S Obua","year":"2005","unstructured":"Obua, S.: Proving bounds for real linear programs in Isabelle\/Hol. In: Hurd, J., Melham, T.F. (eds.) Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, Oxford, UK, 22\u201325 August 2005, Proceedings. Lecture Notes in Computer Science, vol. 3603, pp. 227\u2013244. Springer, New York (2005)"},{"key":"9168_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1007\/978-3-540-74591-4_17","volume-title":"TPHOLs","author":"S Obua","year":"2007","unstructured":"Obua, S.: Proof pearl: looping around the orbit. In: Schneider, K., Brandt, J. (eds.) TPHOLs. Lecture Notes in Computer Science, vol.\u00a04732, pp.\u00a0223\u2013231. Springer, New York (2007)"},{"key":"9168_CR29","unstructured":"Obua, S.: Flyspeck II: the basic linear programs. Ph.D. thesis, Technische Universit\u00e4t M\u00fcnchen (2008)"},{"key":"9168_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"401","DOI":"10.1007\/BFb0055149","volume-title":"TPHOLs","author":"F Puitg","year":"1998","unstructured":"Puitg, F., Dufourd, J.-F.: Formal specification and theorem proving breakthroughs in geometric modeling. In: Grundy, J., Newey, M.C. (eds.) TPHOLs. Lecture Notes in Computer Science, vol. 1479, pp. 401\u2013422. Springer, New York (1998)"}],"container-title":["Annals of Mathematics and Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-009-9168-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10472-009-9168-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-009-9168-z","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,17]],"date-time":"2024-03-17T13:57:13Z","timestamp":1710683833000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10472-009-9168-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,8]]},"references-count":30,"journal-issue":{"issue":"3-4","published-print":{"date-parts":[[2009,8]]}},"alternative-id":["9168"],"URL":"https:\/\/doi.org\/10.1007\/s10472-009-9168-z","relation":{},"ISSN":["1012-2443","1573-7470"],"issn-type":[{"value":"1012-2443","type":"print"},{"value":"1573-7470","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,8]]}}}