{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,22]],"date-time":"2025-06-22T04:04:30Z","timestamp":1750565070530,"version":"3.41.0"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319630458"},{"type":"electronic","value":"9783319630465"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-63046-5_18","type":"book-chapter","created":{"date-parts":[[2017,7,10]],"date-time":"2017-07-10T13:34:07Z","timestamp":1499693647000},"page":"291-309","source":"Crossref","is-referenced-by-count":1,"title":["Splitting Proofs for Interpolation"],"prefix":"10.1007","author":[{"given":"Bernhard","family":"Gleiss","sequence":"first","affiliation":[]},{"given":"Laura","family":"Kov\u00e1cs","sequence":"additional","affiliation":[]},{"given":"Martin","family":"Suda","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,7,11]]},"reference":[{"key":"18_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1007\/978-3-642-28717-6_7","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"F Alberti","year":"2012","unstructured":"Alberti, F., Bruttomesso, R., Ghilardi, S., Ranise, S., Sharygina, N.: Lazy abstraction with interpolants for arrays. In: Bj\u00f8rner, N., Voronkov, A. (eds.) LPAR 2012. LNCS, vol. 7180, pp. 46\u201361. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-28717-6_7"},{"issue":"1","key":"18_CR2","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1007\/s10817-014-9314-0","volume":"54","author":"MP Bonacina","year":"2015","unstructured":"Bonacina, M.P., Johansson, M.: On interpolation in automated theorem proving. J. Autom. Reasoning 54(1), 69\u201397 (2015)","journal-title":"J. Autom. Reasoning"},{"key":"18_CR3","unstructured":"Christ, J., Hoenicke, J.: Instantiation-based interpolation for quantified formulae. In: Decision Procedures in Software, Hardware and Bioware, April 18\u201323 April 2010, vol. 10161. Dagstuhl Seminar Proceedings. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, Germany (2010)"},{"issue":"1","key":"18_CR4","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1007\/s10817-016-9365-5","volume":"57","author":"J Christ","year":"2016","unstructured":"Christ, J., Hoenicke, J.: Proof tree preserving tree interpolation. J. Autom. Reasoning 57(1), 67\u201395 (2016)","journal-title":"J. Autom. Reasoning"},{"key":"18_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1007\/978-3-540-78800-3_30","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Cimatti","year":"2008","unstructured":"Cimatti, A., Griggio, A., Sebastiani, R.: Efficient interpolant generation in satisfiability modulo theories. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 397\u2013412. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-78800-3_30"},{"issue":"3","key":"18_CR6","doi-asserted-by":"crossref","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. J. Symb. Log. 22(3), 250\u2013268 (1957)","journal-title":"J. Symb. Log."},{"key":"18_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Moura","year":"2008","unstructured":"Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-78800-3_24"},{"key":"18_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"737","DOI":"10.1007\/978-3-319-08867-9_49","volume-title":"Computer Aided Verification","author":"B Dutertre","year":"2014","unstructured":"Dutertre, B.: Yices\u00a02.2. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 737\u2013744. Springer, Cham (2014). doi: 10.1007\/978-3-319-08867-9_49"},{"key":"18_CR9","doi-asserted-by":"crossref","unstructured":"Hoder, K., Kov\u00e1cs, L., Voronkov, A.: Playing in the grey area of proofs. In: Principles of Programming Languages, pp. 259\u2013272. ACM (2012)","DOI":"10.1145\/2103621.2103689"},{"key":"18_CR10","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., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 459\u2013473. Springer, Heidelberg (2006). doi: 10.1007\/11691372_33"},{"key":"18_CR11","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/978-3-642-02959-2_17","volume-title":"Automated Deduction \u2013 CADE-22","author":"L Kov\u00e1cs","year":"2009","unstructured":"Kov\u00e1cs, L., Voronkov, A.: Interpolation and symbol elimination. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol. 5663, pp. 199\u2013213. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-02959-2_17"},{"key":"18_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-39799-8_1","volume-title":"Computer Aided Verification","author":"L Kov\u00e1cs","year":"2013","unstructured":"Kov\u00e1cs, L., Voronkov, A.: First-order theorem proving and Vampire. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 1\u201335. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-39799-8_1"},{"key":"18_CR13","doi-asserted-by":"crossref","unstructured":"Kov\u00e1cs, L., Voronkov, A.: First-order interpolation and interpolating proof systems. In: LPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, vol. 46. EPiC Series in Computing, pp. 49\u201364. EasyChair (2017)","DOI":"10.29007\/1qb8"},{"key":"18_CR14","unstructured":"Lahiri, S.K., Mehra, K.K.: Interpolant based decision procedure for quantifier-free Presburger arithmetic. Technical Report MSR-TR-2005-121, Microsoft Research (2005)"},{"key":"18_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-45069-6_1","volume-title":"Computer Aided Verification","author":"KL McMillan","year":"2003","unstructured":"McMillan, K.L.: Interpolation and SAT-based model checking. In: Hunt, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 1\u201313. Springer, Heidelberg (2003). doi: 10.1007\/978-3-540-45069-6_1"},{"key":"18_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/11817963_14","volume-title":"Computer Aided Verification","author":"KL McMillan","year":"2006","unstructured":"McMillan, K.L.: Lazy abstraction with interpolants. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 123\u2013136. Springer, Heidelberg (2006). doi: 10.1007\/11817963_14"},{"key":"18_CR17","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":"KL 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. 4963, pp. 413\u2013427. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-78800-3_31"},{"key":"18_CR18","doi-asserted-by":"crossref","unstructured":"Nonnengart, A., Weidenbach, C.: Computing small clause normal forms. In: Handbook of Automated Reasoning, vol. 2s, pp. 335\u2013367. Elsevier and MIT Press (2001)","DOI":"10.1016\/B978-044450813-3\/50008-4"},{"key":"18_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-319-41135-4_9","volume-title":"Tests and Proofs","author":"A Podelski","year":"2016","unstructured":"Podelski, A., Sch\u00e4f, M., Wies, T.: Classifying bugs with interpolants. In: Aichernig, B.K.K., Furia, C.A.A. (eds.) TAP 2016. LNCS, vol. 9762, pp. 151\u2013168. Springer, Cham (2016). doi: 10.1007\/978-3-319-41135-4_9"},{"key":"18_CR20","doi-asserted-by":"crossref","unstructured":"Reger, G., Suda, M., Voronkov, A.: New techniques in clausal form generation. In: GCAI 2016, 2nd Global Conference on Artificial Intelligence, vol. 41. EPiC Series in Computing, pp. 11\u201323. EasyChair (2016)","DOI":"10.29007\/dzfz"},{"key":"18_CR21","unstructured":"Stump, A., Sutcliffe, G., Tinelli, C.: StarExec, a cross community logic solving service (2012). https:\/\/www.starexec.org"},{"issue":"4","key":"18_CR22","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/s10817-009-9143-8","volume":"43","author":"G Sutcliffe","year":"2009","unstructured":"Sutcliffe, G.: The TPTP problem library and associated infrastructure. J. Autom. Reasoning 43(4), 337\u2013362 (2009)","journal-title":"J. Autom. Reasoning"},{"key":"18_CR23","doi-asserted-by":"crossref","unstructured":"Totla, N., Wies, T.: Complete instantiation-based interpolation. In: Principles of Programming Languages, pp. 537\u2013548. ACM (2013)","DOI":"10.1145\/2429069.2429132"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 26"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-63046-5_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,21]],"date-time":"2025-06-21T19:24:47Z","timestamp":1750533887000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-63046-5_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319630458","9783319630465"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-63046-5_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}