{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T02:03:53Z","timestamp":1760061833776,"version":"3.40.3"},"publisher-location":"Cham","reference-count":13,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319214009"},{"type":"electronic","value":"9783319214016"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-21401-6_42","type":"book-chapter","created":{"date-parts":[[2015,7,24]],"date-time":"2015-07-24T10:13:46Z","timestamp":1437732826000},"page":"623-637","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Linear Integer Arithmetic Revisited"],"prefix":"10.1007","author":[{"given":"Martin","family":"Bromberger","sequence":"first","affiliation":[]},{"given":"Thomas","family":"Sturm","sequence":"additional","affiliation":[]},{"given":"Christoph","family":"Weidenbach","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,7,25]]},"reference":[{"key":"42_CR1","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/11916277_35","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"CW Barrett","year":"2006","unstructured":"Barrett, C.W., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Splitting on demand in SAT modulo theories. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol. 4246, pp. 512\u2013526. Springer, Heidelberg (2006)"},{"doi-asserted-by":"crossref","unstructured":"Bromberger, M., Sturm, T., Weidenbach, C.: Linear integer arithmetic revisited. ArXiv e-prints, abs\/1503.02948 (2015)","key":"42_CR2","DOI":"10.1007\/978-3-319-21401-6_42"},{"unstructured":"Cooper, D.C.: Theorem proving in arithmetic without multiplication. In: Meltzer, B., Michie, D. (eds.) 1971 Proceedings of the Seventh Annual Machine Intelligence Workshop, Edinburgh. Machine Intelligence, vol. 7, pp. 91\u201399. Edinburgh University Press (1972)","key":"42_CR3"},{"key":"42_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-642-02658-4_20","volume-title":"Computer Aided Verification","author":"I Dillig","year":"2009","unstructured":"Dillig, I., Dillig, T., Aiken, A.: Cuts from proofs: a complete and practical technique for solving linear inequalities over integers. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 233\u2013247. Springer, Heidelberg (2009)"},{"issue":"4","key":"42_CR5","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1007\/s11786-012-0134-5","volume":"6","author":"A Fietzke","year":"2012","unstructured":"Fietzke, A., Weidenbach, C.: Superposition as a decision procedure for timed automata. Math. Comput. Sci. 6(4), 409\u2013425 (2012)","journal-title":"Math. Comput. Sci."},{"key":"42_CR6","first-page":"27","volume":"7","author":"MJ Fischer","year":"1974","unstructured":"Fischer, M.J., Rabin, M.: Super-exponential complexity of Presburger arithmetic. SIAM-AMS Proc. 7, 27\u201341 (1974)","journal-title":"SIAM-AMS Proc."},{"issue":"1\/2","key":"42_CR7","first-page":"1","volume":"8","author":"A Griggio","year":"2012","unstructured":"Griggio, A.: A practical approach to satisability modulo linear integer arithmetic. JSAT 8(1\/2), 1\u201327 (2012)","journal-title":"JSAT"},{"issue":"1","key":"42_CR8","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/s10817-013-9281-x","volume":"51","author":"D Jovanovi\u0107","year":"2013","unstructured":"Jovanovi\u0107, D., de Moura, L.: Cutting to the chase. J. Autom. Reasoning 51(1), 79\u2013108 (2013)","journal-title":"J. Autom. Reasoning"},{"volume-title":"50 Years of Integer Programming 1958\u20132008","year":"2010","unstructured":"J\u00fcnger, M., Liebling, T.M., Naddef, D., Nemhauser, G.L., Pulleyblank, W.R., Reinelt, G., Rinaldi, G., Wolsey, L.A. (eds.): 50 Years of Integer Programming 1958\u20132008. Springer, Heidelberg (2010)","key":"42_CR9"},{"issue":"6","key":"42_CR10","doi-asserted-by":"publisher","first-page":"545","DOI":"10.1007\/s00200-007-0053-x","volume":"18","author":"A Lasaruk","year":"2007","unstructured":"Lasaruk, A., Sturm, T.: Weak quantifier elimination for the full linear theory of the integers. A uniform generalization of Presburger arithmetic. Appl. Algebra Eng. Commun. Comput. 18(6), 545\u2013574 (2007)","journal-title":"Appl. Algebra Eng. Commun. Comput."},{"issue":"4","key":"42_CR11","doi-asserted-by":"publisher","first-page":"765","DOI":"10.1145\/322276.322287","volume":"28","author":"CH Papadimitriou","year":"1981","unstructured":"Papadimitriou, C.H.: On the complexity of integer programming. J. ACM 28(4), 765\u2013768 (1981)","journal-title":"J. ACM"},{"unstructured":"Presburger, M.: \u00dcber die Vollst\u00e4ndigkeit eines gewissen Systems der Arithmetik ganzer Zahlen. welchem die Addition als einzige Operation hervortritt. In: Comptes Rendus du premier congres de Mathematiciens des Pays Slaves, pp. 92\u2013101. Warsaw, Poland (1929)","key":"42_CR12"},{"issue":"5","key":"42_CR13","doi-asserted-by":"publisher","first-page":"395","DOI":"10.1016\/S0747-7171(08)80051-X","volume":"10","author":"V Weispfenning","year":"1990","unstructured":"Weispfenning, V.: The complexity of almost linear diophantine problems. J. Symb. Comput. 10(5), 395\u2013403 (1990)","journal-title":"J. Symb. Comput."}],"container-title":["Lecture Notes in Computer Science","Automated Deduction - CADE-25"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-21401-6_42","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,21]],"date-time":"2023-02-21T09:47:27Z","timestamp":1676972847000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-21401-6_42"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319214009","9783319214016"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-21401-6_42","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"25 July 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}