{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,26]],"date-time":"2025-08-26T07:08:07Z","timestamp":1756192087424},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540283720"},{"type":"electronic","value":"9783540318200"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11541868_15","type":"book-chapter","created":{"date-parts":[[2010,7,20]],"date-time":"2010-07-20T15:12:52Z","timestamp":1279638772000},"page":"227-244","source":"Crossref","is-referenced-by-count":19,"title":["Proving Bounds for Real Linear Programs in Isabelle\/HOL"],"prefix":"10.1007","author":[{"given":"Steven","family":"Obua","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"15_CR1","unstructured":"Hales, T.C.: Some algorithms arising in the proof of the Kepler conjecture, sect. 3.1.1., arXiv:math.MG\/0205209"},{"key":"15_CR2","unstructured":"Hales, T.C.: A Proof of the Kepler Conjecture. Annals of Mathematics (to appear)"},{"key":"15_CR3","unstructured":"The Flyspeck Project Fact Sheet. \n                    \n                      http:\/\/www.math.pitt.edu\/~thales\/flyspeck\/index.html"},{"key":"15_CR4","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. Springer, Heidelberg (2002)"},{"key":"15_CR5","volume-title":"Theory of Linear and Integer Programming","author":"A. Schrijver","year":"1986","unstructured":"Schrijver, A.: Theory of Linear and Integer Programming. Wiley & Sons, Chichester (1986)"},{"key":"15_CR6","doi-asserted-by":"crossref","unstructured":"Paulson, L.C.: Organizing Numerical Theories Using Axiomatic Type Classes. Journal of Automated Reasoning (in press)","DOI":"10.1007\/s10817-004-3997-6"},{"key":"15_CR7","doi-asserted-by":"crossref","unstructured":"Paulson, L.C.: Defining Functions on Equivalence Classes. ACM Transactions on Computational Logic (in press)","DOI":"10.1145\/1183278.1183280"},{"key":"15_CR8","doi-asserted-by":"crossref","unstructured":"Two Fast Algorithms for Sparse Matrices: Multiplication and Permuted Transposition. ACM Transactions on Mathematical Software\u00a04(3), 250\u2013269 (1978)","DOI":"10.1145\/355791.355796"},{"key":"15_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/3-540-44659-1_2","volume-title":"Theorem Proving in Higher Order Logics","author":"B. Barras","year":"2000","unstructured":"Barras, B.: Programming and Computing in HOL. In: Aagaard, M.D., Harrison, J. (eds.) TPHOLs 2000 LNCS, vol.\u00a01869, pp. 17\u201337. Springer, Heidelberg (2000)"},{"key":"15_CR10","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/BFb0037108","volume-title":"Typed Lambda Calculi and Applications","author":"B. Jacobs","year":"1993","unstructured":"Jacobs, B., Melham, T.: Translating Dependent Type Theory into Higher Order Logic. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993, vol.\u00a0664, pp. 209\u2013229. Springer, Heidelberg (1993)"},{"key":"15_CR11","volume-title":"Algebra","author":"S. Lang","year":"1974","unstructured":"Lang, S.: Algebra. Addison-Wesley, Reading (1974)"},{"key":"15_CR12","unstructured":"Birkhoff, G.: Lattice Theory. AMS (1967)"},{"key":"15_CR13","volume-title":"Partially ordered algebraic systems","author":"L. Fuchs","year":"1963","unstructured":"Fuchs, L.: Partially ordered algebraic systems. Addison-Wesley, Reading (1963)"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11541868_15.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T15:18:11Z","timestamp":1605626291000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11541868_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540283720","9783540318200"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/11541868_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}