{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T22:29:51Z","timestamp":1725575391077},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642182747"},{"type":"electronic","value":"9783642182754"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-18275-4_8","type":"book-chapter","created":{"date-parts":[[2011,1,17]],"date-time":"2011-01-17T00:06:38Z","timestamp":1295222798000},"page":"88-102","source":"Crossref","is-referenced-by-count":16,"title":["Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic"],"prefix":"10.1007","author":[{"given":"Angelo","family":"Brillout","sequence":"first","affiliation":[]},{"given":"Daniel","family":"Kroening","sequence":"additional","affiliation":[]},{"given":"Philipp","family":"R\u00fcmmer","sequence":"additional","affiliation":[]},{"given":"Thomas","family":"Wahl","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"3","key":"8_CR1","doi-asserted-by":"publisher","first-page":"250","DOI":"10.2307\/2963593","volume":"22","author":"W. Craig","year":"1957","unstructured":"Craig, W.: Linear reasoning. A new form of the Herbrand-Gentzen theorem. The Journal of Symbolic Logic\u00a022(3), 250\u2013268 (1957)","journal-title":"The Journal of Symbolic Logic"},{"key":"8_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"384","DOI":"10.1007\/978-3-642-14203-1_33","volume-title":"Automated Reasoning","author":"A. Brillout","year":"2010","unstructured":"Brillout, A., Kroening, D., R\u00fcmmer, P., Wahl, T.: An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS, vol.\u00a06173, pp. 384\u2013399. Springer, Heidelberg (2010)"},{"key":"8_CR3","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-2360-3","volume-title":"First-Order Logic and Automated Theorem Proving","author":"M.C. Fitting","year":"1996","unstructured":"Fitting, M.C.: First-Order Logic and Automated Theorem Proving, 2nd edn. Springer, Heidelberg (1996)","edition":"2"},{"key":"8_CR4","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1145\/1066100.1066102","volume":"52","author":"D. Detlefs","year":"2005","unstructured":"Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: A theorem prover for program checking. Journal of the ACM\u00a052, 365\u2013473 (2005)","journal-title":"Journal of the ACM"},{"key":"8_CR5","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1007\/978-3-540-89439-1_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"P. R\u00fcmmer","year":"2008","unstructured":"R\u00fcmmer, P.: A constraint sequent calculus for first-order logic with linear integer arithmetic. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol.\u00a05330, pp. 274\u2013289. Springer, Heidelberg (2008)"},{"key":"8_CR6","unstructured":"R\u00fcmmer, P.: Calculi for Program Incorrectness and Arithmetic. PhD thesis, University of Gothenburg (2008)"},{"key":"8_CR7","doi-asserted-by":"crossref","unstructured":"Halpern, J.Y.: Presburger arithmetic with unary predicates is ${\\Pi_1^1}$ complete. Journal of Symbolic Logic\u00a056 (1991)","DOI":"10.2307\/2274706"},{"key":"8_CR8","doi-asserted-by":"crossref","unstructured":"Brillout, A., Kroening, D., R\u00fcmmer, P., Wahl, T.: Beyond quantifier-free interpolation in extensions of Presburger arithmetic (extended Technical Report). Technical report, CoRR abs\/1011.1036 (2010)","DOI":"10.1007\/978-3-642-18275-4_8"},{"key":"8_CR9","volume-title":"Information Processing 1962: Proceedings IFIP Congress 1962","author":"J. McCarthy","year":"1963","unstructured":"McCarthy, J.: Towards a mathematical science of computation. In: Information Processing 1962: Proceedings IFIP Congress 1962, North-Holland, Amsterdam (1963)"},{"key":"8_CR10","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: An interpolating theorem prover. Theor. Comput. Sci. 345 (2005)","DOI":"10.1016\/j.tcs.2005.07.003"},{"key":"8_CR11","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1145\/1181775.1181789","volume-title":"SIGSOFT 2006\/FSE-14","author":"D. Kapur","year":"2006","unstructured":"Kapur, D., Majumdar, R., Zarba, C.G.: Interpolation for data structures. In: SIGSOFT 2006\/FSE-14, pp. 105\u2013116. ACM, New York (2006)"},{"key":"8_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"459","DOI":"10.1007\/11691372_33","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R. Jhala","year":"2006","unstructured":"Jhala, R., McMillan, K.L.: A practical and complete approach to predicate refinement. In: Hermanns, H. (ed.) TACAS 2006. LNCS, vol.\u00a03920, pp. 459\u2013473. Springer, Heidelberg (2006)"},{"key":"8_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1007\/978-3-540-78800-3_31","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K.L. McMillan","year":"2008","unstructured":"McMillan, K.L.: Quantified invariant generation using an interpolating saturation prover. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 413\u2013427. Springer, Heidelberg (2008)"},{"key":"8_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/11609773_28","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A.R. Bradley","year":"2005","unstructured":"Bradley, A.R., Manna, Z., Sipma, H.B.: What\u2019s decidable about arrays? In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol.\u00a03855, pp. 427\u2013442. Springer, Heidelberg (2005)"},{"key":"8_CR15","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1007\/11532231_26","volume-title":"Automated Deduction \u2013 CADE-20","author":"G. Yorsh","year":"2005","unstructured":"Yorsh, G., Musuvathi, M.: A combination method for generating interpolants. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol.\u00a03632, pp. 353\u2013368. Springer, Heidelberg (2005)"},{"key":"8_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1007\/978-3-642-00768-2_34","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Fuchs","year":"2009","unstructured":"Fuchs, A., Goel, A., Grundy, J., Krsti\u0107, S., Tinelli, C.: Ground interpolation for the theory of equality. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol.\u00a05505, pp. 413\u2013427. Springer, Heidelberg (2009)"},{"key":"8_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/978-3-642-11319-2_12","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"V. D\u2019Silva","year":"2010","unstructured":"D\u2019Silva, V., Purandare, M., Weissenbacher, G., Kroening, D.: Interpolant Strength. In: Barthe, G., Hermenegildo, M. (eds.) VMCAI 2010. LNCS, vol.\u00a05944, pp. 129\u2013145. Springer, Heidelberg (2010)"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-18275-4_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,7]],"date-time":"2019-06-07T18:39:32Z","timestamp":1559932772000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-18275-4_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642182747","9783642182754"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-18275-4_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}