{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,1]],"date-time":"2026-04-01T10:09:59Z","timestamp":1775038199456,"version":"3.50.1"},"reference-count":89,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2015,3,20]],"date-time":"2015-03-20T00:00:00Z","timestamp":1426809600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2015,4]]},"DOI":"10.1007\/s10817-015-9325-5","type":"journal-article","created":{"date-parts":[[2015,3,19]],"date-time":"2015-03-19T03:19:53Z","timestamp":1426735193000},"page":"353-390","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["Interpolation Systems for Ground Proofs in Automated Deduction: a Survey"],"prefix":"10.1007","volume":"54","author":[{"given":"Maria Paola","family":"Bonacina","sequence":"first","affiliation":[]},{"given":"Moa","family":"Johansson","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,3,20]]},"reference":[{"key":"9325_CR1","first-page":"313","volume-title":"Proceedings of the 25th Conference on Computer Aided Verification (CAV), volume 8044 of Lecture Notes in Computer Science","author":"A Albarghouthi","year":"2013","unstructured":"Albarghouthi, A., McMillan, K.L.: Beautiful interpolants. In: Sharygina, N, Veith, H (eds.) Proceedings of the 25th Conference on Computer Aided Verification (CAV), volume 8044 of Lecture Notes in Computer Science, pp. 313\u2013329. Springer, Berlin (2013)"},{"key":"9325_CR2","doi-asserted-by":"crossref","unstructured":"Alberti, F., Bruttomesso, R., Ghilardi, S., Ranise, S., Sharygina, N.: Lazy abstraction with interpolants for arrays. In: Bj\u00f8rner N, Voronkov, A (eds.) Proceedings of the 18th Conference on Logic, Programming and Automated Reasoning (LPAR), volume 7180 of Lecture Notes in Artificial Intelligence, pp. 46\u201361. Springer, Berlin (2012)","DOI":"10.1007\/978-3-642-28717-6_7"},{"issue":"1","key":"9325_CR3","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1145\/1459010.1459014","volume":"10","author":"A Armando","year":"2009","unstructured":"Armando, A., Bonacina, M.P., Ranise, S., Schulz, S.: New results on rewrite-based satisfiability procedures. ACM Trans. Comput. Log. 10(1), 129\u2013179 (2009)","journal-title":"ACM Trans Comput Log"},{"issue":"2","key":"9325_CR4","doi-asserted-by":"crossref","first-page":"140","DOI":"10.1016\/S0890-5401(03)00020-8","volume":"183","author":"A Armando","year":"2003","unstructured":"Armando, A., Ranise, S., Rusinowitch, M.: A rewriting approach to satisfiability procedures. Inf. Comput. 183(2), 140\u2013164 (2003)","journal-title":"Inf Comput"},{"key":"9325_CR5","first-page":"236","volume-title":"Proceedings of the 14th Conference on Computer Aided Verification (CAV), volume 2404 of Lecture Notes in Computer Science","author":"CW Barrett","year":"2002","unstructured":"Barrett, C.W., Dill, D.L., Stump, A.: Checking satisfiability of first-order formulas by incremental translation to SAT. In: Larsen, K.G., Brinksma, E. (eds.) Proceedings of the 14th Conference on Computer Aided Verification (CAV), volume 2404 of Lecture Notes in Computer Science, pp. 236\u2013249. Springer, Berlin (2002)"},{"key":"9325_CR6","volume-title":"Proceedings of the 4th Workshop on Frontiers of Combining Systems (FroCoS), volume 2309 of Lecture Notes in Computer Science","author":"CW Barrett","year":"2002","unstructured":"Barrett, C.W., Dill, D.L., Stump, A.: A generalization of Shostak\u2019s method for combining decision procedures. In: Armando, A. (ed.) Proceedings of the 4th Workshop on Frontiers of Combining Systems (FroCoS), volume 2309 of Lecture Notes in Computer Science. Springer, Berlin (2002)"},{"key":"9325_CR7","first-page":"304","volume-title":"Proceedings of the 20th Conference on Computer Aided Verification (CAV), volume 5123 of Lecture Notes in Computer Science","author":"D Beyer","year":"2008","unstructured":"Beyer, D., Zufferey, D., Majumdar, R.: CSIsat: interpolation for LA+EUF. In: Gupta, A., Malik, S. (eds.) Proceedings of the 20th Conference on Computer Aided Verification (CAV), volume 5123 of Lecture Notes in Computer Science, pp. 304\u2013308. Springer, Berlin (2008)"},{"key":"9325_CR8","first-page":"1","volume-title":"Proceedings of the 12th International Symposium on Principles and Practice of Declarative Programming (PPDP)","author":"MP Bonacina","year":"2010","unstructured":"Bonacina, M.P.: On theorem proving for program checking \u2013 historical perspective and recent developments. In: Fernandez, M. (ed.) Proceedings of the 12th International Symposium on Principles and Practice of Declarative Programming (PPDP), pp. 1\u201311. ACM, New York (2010)"},{"issue":"1","key":"9325_CR9","doi-asserted-by":"crossref","first-page":"180","DOI":"10.1145\/1182613.1182619","volume":"8","author":"MP Bonacina","year":"2007","unstructured":"Bonacina, M.P., Dershowitz, N.: Abstract canonical inference. ACM Trans. Comput. Log. 8(1), 180\u2013208 (2007)","journal-title":"ACM Trans. Comput. Log."},{"key":"9325_CR10","first-page":"55","volume-title":"Proceedings of the 4th Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR 2006), volume 174(8) of Electronic Notes in Theoretical Computer Science","author":"MP Bonacina","year":"2007","unstructured":"Bonacina, M.P., Echenim, M.: Rewrite-based satisfiability procedures for recursive data structures. In: Cook, B., Sebastiani, R. (eds.) Proceedings of the 4th Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR 2006), volume 174(8) of Electronic Notes in Theoretical Computer Science, pp. 55\u201370. Elsevier, Amsterdam (2007)"},{"issue":"1","key":"9325_CR11","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1093\/logcom\/exm055","volume":"18","author":"MP Bonacina","year":"2008","unstructured":"Bonacina, M.P., Echenim, M.: On variable-inactivity and polynomial T $\\mathcal {T}$ -satisfiability procedures. J. Log. Comput. 18(1), 77\u201396 (2008)","journal-title":"J. Log. Comput."},{"key":"9325_CR12","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1006\/inco.1998.2739","volume":"147","author":"MP Bonacina","year":"1998","unstructured":"Bonacina, M.P., Hsiang, J.: On the modelling of search in theorem proving \u2013 towards a theory of strategy analysis. Inf. Comput. 147, 171\u2013208 (1998)","journal-title":"Inf. Comput."},{"key":"9325_CR13","first-page":"1","volume-title":"Proceedings of the 20th International Conference on Analytic Tableaux and Related Methods (TABLEAUX), volume 6793 of Lecture Notes in Artificial Intelligence","author":"MP Bonacina","year":"2011","unstructured":"Bonacina, M.P., Johansson, M.: On interpolation in decision procedures. In: Br\u00fcnnler, K., Metcalfe, G. (eds.) Proceedings of the 20th International Conference on Analytic Tableaux and Related Methods (TABLEAUX), volume 6793 of Lecture Notes in Artificial Intelligence, pp. 1\u201316. Springer, Berlin (2011)"},{"key":"9325_CR14","first-page":"9","volume-title":"Notes of the 9th International Workshop on Satisfiability Modulo Theories (SMT), number UCB\/EECS-2011-80 in Technical Reports","author":"MP Bonacina","year":"2011","unstructured":"Bonacina, M.P., Johansson, M.: Towards interpolation in an SMT solver with integrated superposition. In: Lahiri, S., Seshia, S. A. (eds.) Notes of the 9th International Workshop on Satisfiability Modulo Theories (SMT), number UCB\/EECS-2011-80 in Technical Reports, pp. 9\u201318. Department of EECS, University of California at Berkeley, Berkeley (2011)"},{"issue":"1","key":"9325_CR15","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. Reason. 54(1), 69\u201397 (2015)","journal-title":"J. Autom. Reason."},{"key":"9325_CR16","volume-title":"The calculus of computation \u2013 decision procedures with applications to verification","author":"AR Bradley","year":"2007","unstructured":"Bradley, A.R., Manna, Z.: The calculus of computation \u2013 decision procedures with applications to verification. Springer, Berlin (2007)"},{"key":"9325_CR17","first-page":"384","volume-title":"Proceedings of the 5th International Joint Conference on Automated Reasoning (IJCAR), volume 6173 of Lecture Notes in Artificial Intelligence","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.) Proceedings of the 5th International Joint Conference on Automated Reasoning (IJCAR), volume 6173 of Lecture Notes in Artificial Intelligence, pp. 384\u2013399. Springer, Berlin (2010)"},{"key":"9325_CR18","unstructured":"Brillout, A., Kroening, D., R\u00fcmmer, P., Wahl, T.: Program verification via Craig interpolation for Presburger arithmetic with arrays. Notes of the 6th International Verification Workshop (VERIFY), 2010. Available at http:\/\/www.philipp.ruemmer.org\/"},{"key":"9325_CR19","first-page":"88","volume-title":"Proceedings of the 12th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI), volume 6538 of Lecture Notes in Computer Science","author":"A Brillout","year":"2011","unstructured":"Brillout, A., Kroening, D., R\u00fcmmer, P., Wahl, T.: Beyond quantifier-free interpolation in extensions of Presburger arithmetic. In: Jhala, R., Schmidt, D. (eds.) Proceedings of the 12th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI), volume 6538 of Lecture Notes in Computer Science, pp. 88\u2013102. Springer, Berlin (2011)"},{"key":"9325_CR20","first-page":"103","volume-title":"Proceedings of the 8th Symposium on Frontiers of Combining Systems (FroCoS), volume 6989 of Lecture Notes in Artificial Intelligence","author":"R Bruttomesso","year":"2011","unstructured":"Bruttomesso, R., Ghilardi, S., Ranise, S.: A combination of rewriting and constraint solving for the quantifier-free interpolation of arrays with integer difference constraints. In: Tinelli, C., Sofronie-Stokkermans, V. (eds.) Proceedings of the 8th Symposium on Frontiers of Combining Systems (FroCoS), volume 6989 of Lecture Notes in Artificial Intelligence, pp. 103\u2013118. Springer, Berlin (2011)"},{"key":"9325_CR21","first-page":"118","volume-title":"Proceedings of the 6th International Joint Conference on Automated Reasoning (IJCAR), volume 7364 of Lecture Notes in Artificial Intelligence","author":"R Bruttomesso","year":"2012","unstructured":"Bruttomesso, R., Ghilardi, S., Ranise, S.: From strong amalgamability to modularity of quantifier-free interpolation. In: Gramlich, B., Miller, D., Sattler, U. (eds.) Proceedings of the 6th International Joint Conference on Automated Reasoning (IJCAR), volume 7364 of Lecture Notes in Artificial Intelligence, pp. 118\u2013133. Springer, Berlin (2012)"},{"key":"9325_CR22","doi-asserted-by":"crossref","unstructured":"Bruttomesso, R., Ghilardi, S., Ranise, S.: Quantifier-free interpolation for a theory of arrays. Logical Methods Comput. Sci. 8(2) (2012)","DOI":"10.2168\/LMCS-8(2:4)2012"},{"key":"9325_CR23","doi-asserted-by":"crossref","unstructured":"Bruttomesso, R., Ghilardi, S., Ranise, S.: Quantifier-free interpolation in combinations of equality interpolating theories. ACM Trans. Comput. Log. 15(1) (2014)","DOI":"10.1145\/2490253"},{"key":"9325_CR24","first-page":"770","volume-title":"Flexible interpolation generation in satisfiability modulo theories. In: Proceedings of the 14th International Conference on Computer-Aided Design (ICCAD)","author":"R Bruttomesso","year":"2010","unstructured":"Bruttomesso, R., Rollini, S.F., Sharygina, N., Tsitovich, A.: Flexible interpolation generation in satisfiability modulo theories. In: Proceedings of the 14th International Conference on Computer-Aided Design (ICCAD), pp. 770\u2013777. IEEE, Los Alamitos (2010)"},{"key":"9325_CR25","unstructured":"Christ, J., Hoenicke, J.: Instantiation-based interpolation for quantified formulae. Notes of the 8th International Workshop on Satisfiability Modulo Theories (SMT) (2010)"},{"issue":"1","key":"9325_CR26","doi-asserted-by":"crossref","first-page":"Article 7","DOI":"10.1145\/1838552.1838559","volume":"12","author":"A Cimatti","year":"2010","unstructured":"Cimatti, A., Griggio, A., Sebastiani, R.: Efficient generation of Craig interpolants in satisfiability modulo theories. ACM Trans. Comput. Log. 12(1), Article 7 (2010)","journal-title":"ACM Trans. Comput. Log."},{"issue":"1","key":"9325_CR27","doi-asserted-by":"crossref","first-page":"36","DOI":"10.2307\/2273702","volume":"44","author":"SA Cook","year":"1979","unstructured":"Cook, S.A., Reckhow, R.A.: The relative efficiency of propositional proof systems. J. Symb. Log. 44(1), 36\u201350 (1979)","journal-title":"J. Symb. Log."},{"issue":"3","key":"9325_CR28","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."},{"issue":"7","key":"9325_CR29","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Comm. ACM 5(7), 394\u2013397 (1962)","journal-title":"Comm. ACM"},{"key":"9325_CR30","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M Davis","year":"1960","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM 7, 201\u2013215 (1960)","journal-title":"J. ACM"},{"key":"9325_CR31","first-page":"183","volume-title":"Proceedings of the 21st Conference on Automated Deduction (CADE), volume 4603 of Lecture Notes in Artificial Intelligence","author":"L de Moura","year":"2007","unstructured":"de Moura, L., Bj\u00f8rner, N.: Efficient E-matching for SMT-solvers. In: Pfenning, F. (ed.) Proceedings of the 21st Conference on Automated Deduction (CADE), volume 4603 of Lecture Notes in Artificial Intelligence, pp. 183\u2013198. Springer, Berlin (2007)"},{"key":"9325_CR32","first-page":"400","volume-title":"Proceedings of the 5th International Joint Conference on Automated Reasoning (IJCAR), volume 6173 of Lecture Notes in Artificial Intelligence","author":"L de Moura","year":"2010","unstructured":"de Moura, L., Bj\u00f8rner, N.: Bugs, moles and skeletons: Symbolic reasoning for software development. In: Giesl, J., H\u00e4hnle, R. (eds.) Proceedings of the 5th International Joint Conference on Automated Reasoning (IJCAR), volume 6173 of Lecture Notes in Artificial Intelligence, pp. 400\u2013411. Springer, Berlin (2010)"},{"issue":"9","key":"9325_CR33","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1145\/1995376.1995394","volume":"54","author":"L de Moura","year":"2011","unstructured":"de Moura, L., Bj\u00f8rner, N.: Satisfiability modulo theories: introduction and applications. Comm. ACM 54(9), 69\u201377 (2011)","journal-title":"Comm. ACM"},{"key":"9325_CR34","doi-asserted-by":"crossref","first-page":"535","DOI":"10.1016\/B978-044450813-3\/50011-4","volume-title":"Handbook of automated reasoning, vol. 1","author":"N Dershowitz","year":"2001","unstructured":"Dershowitz, N., Plaisted, D.A.: Rewriting. In: Robinson, A., Voronkov, A. (eds.) Handbook of automated reasoning, vol. 1, pp. 535\u2013610. Elsevier, Amsterdam (2001)"},{"issue":"3","key":"9325_CR35","doi-asserted-by":"crossref","first-page":"365","DOI":"10.1145\/1066100.1066102","volume":"52","author":"DL Detlefs","year":"2005","unstructured":"Detlefs, D.L., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. J. ACM 52(3), 365\u2013473 (2005)","journal-title":"J. ACM"},{"key":"9325_CR36","first-page":"185","volume-title":"Proceedings of the 19th European Symposium on Programming (ESOP), volume 6012 of Lecture Notes in Computer Science","author":"V D\u2019Silva","year":"2010","unstructured":"D\u2019Silva, V.: Propositional interpolation and abstract interpretation. In: Gordon, A.D. (ed.) Proceedings of the 19th European Symposium on Programming (ESOP), volume 6012 of Lecture Notes in Computer Science, pp. 185\u2013204. Springer, Berlin (2010)"},{"key":"9325_CR37","first-page":"129","volume-title":"Proceedings of the 11th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), volume 5944 of Lecture Notes in Computer Science","author":"V D\u2019Silva","year":"2010","unstructured":"D\u2019Silva, V., Kroening, D., Purandare, M., Weissenbacher, G.: Interpolant strength. In: Barthe, G., Hermenegildo, M.V. (eds.) Proceedings of the 11th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), volume 5944 of Lecture Notes in Computer Science, pp. 129\u2013145. Springer, Berlin (2010)"},{"key":"9325_CR38","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-2360-3","volume-title":"First-order logic and automated theorem proving","author":"M Fitting","year":"1996","unstructured":"Fitting, M.: First-order logic and automated theorem proving. Springer, Berlin (1996)"},{"key":"9325_CR39","doi-asserted-by":"crossref","unstructured":"Fuchs, A., Goel, A., Grundy, J., Krsti\u0107, S., Tinelli, C.: Ground interpolation for the theory of equality. Logical Methods Comput. Sci. 8(1) (2012)","DOI":"10.2168\/LMCS-8(1:6)2012"},{"key":"9325_CR40","volume-title":"Logic for computer science \u2013 foundations of automatic theorem proving","author":"J Gallier","year":"1987","unstructured":"Gallier, J.: Logic for computer science \u2013 foundations of automatic theorem proving. Wiley, New York (1987)"},{"issue":"10","key":"9325_CR41","doi-asserted-by":"crossref","first-page":"1453","DOI":"10.1016\/j.ic.2005.10.002","volume":"240","author":"H Ganzinger","year":"2006","unstructured":"Ganzinger, H., Sofronie-Stokkermans, V., Waldmann, U.: Modular proof systems for partial functions with Evans equality. Inf. Comput. 240(10), 1453\u20131492 (2006)","journal-title":"Inf. Comput."},{"key":"9325_CR42","first-page":"167","volume-title":"Proceedings of the 21st conference on automated deduction (CADE), volume 4603 of Lecture Notes in Artificial Intelligence","author":"Y Ge","year":"2007","unstructured":"Ge, Y., Barrett, C., Tinelli, C.: Solving quantified verification conditions using satisfiability modulo theories. In: Pfenning, F. (ed.) Proceedings of the 21st conference on automated deduction (CADE), volume 4603 of Lecture Notes in Artificial Intelligence, pp. 167\u2013182. Springer, Berlin (2007)"},{"key":"9325_CR43","first-page":"306","volume-title":"Proceedings of the 21st conference on computer aided verification (CAV), volume 5643 of Lecture Notes in Computer Science","author":"Y Ge","year":"2009","unstructured":"Ge, Y., de Moura, L.: Complete instantiation for quantified formulas in satisfiability modulo theories. In: Bouajjani, A., Maler, O. (eds.) Proceedings of the 21st conference on computer aided verification (CAV), volume 5643 of Lecture Notes in Computer Science, pp. 306\u2013320. Springer, Berlin (2009)"},{"key":"9325_CR44","unstructured":"Givan, R., McAllester, D.: Proceedings of the 3rd international conference on principles of knowledge representation and reasoning (KR). In: Nebel, B., Rich, C., Swartout, W. R. (eds.) , pp. 403\u2013412. Morgan Kaufmann (1992)"},{"key":"9325_CR45","first-page":"183","volume-title":"Proceedings of the 22nd Conference on Automated Deduction (CADE), volume 5663 of Lecture Notes in Artificial Intelligence","author":"A Goel","year":"2009","unstructured":"Goel, A., Krsti\u0107, S., Tinelli, C.: Ground interpolation for combined theories. In: Schmidt, R. (ed.) Proceedings of the 22nd Conference on Automated Deduction (CADE), volume 5663 of Lecture Notes in Artificial Intelligence, pp. 183\u2013198. Springer, Berlin (2009)"},{"key":"9325_CR46","volume-title":"Proceedings of the 11th Conference on Formal Methods in Computer Aided Design (FMCAD)","author":"A Griggio","year":"2011","unstructured":"Griggio, A.: Effective word-level interpolation for software verification. In: Bjesse, P., Slobodova, A. (eds.) Proceedings of the 11th Conference on Formal Methods in Computer Aided Design (FMCAD). ACM and IEEE, New York (2011)"},{"key":"9325_CR47","volume-title":"Proceedings of the 9th Asian Symposium on Programming Languages and Systems (APLAS), volume 7078 of Lecture Notes in Computer Science","author":"A Gupta","year":"2011","unstructured":"Gupta, A., Popeea, C., Rybalchenko, A.: Solving recursion-free Horn clauses over LI+UIF. In: Yang, H. (ed.) Proceedings of the 9th Asian Symposium on Programming Languages and Systems (APLAS), volume 7078 of Lecture Notes in Computer Science. Springer, Berlin (2011)"},{"key":"9325_CR48","doi-asserted-by":"crossref","first-page":"232","DOI":"10.1145\/964001.964021","volume-title":"Proceedings of the 31st ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL)","author":"TA Henzinger","year":"2004","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: Leroy, X. (ed.) Proceedings of the 31st ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL), pp. 232\u2013244. ACM, New York (2004)"},{"key":"9325_CR49","first-page":"188","volume-title":"Proceedings of the 5th international joint conference on automated reasoning (IJCAR), volume 6173 of Lecture Notes in Artificial Intelligence","author":"K Hoder","year":"2010","unstructured":"Hoder, K., Kov\u00e0cs, L., Voronkov, A.: Interpolation and symbol elimination in Vampire. In: Giesl, J., H\u00e4hnle, R. (eds.) Proceedings of the 5th international joint conference on automated reasoning (IJCAR), volume 6173 of Lecture Notes in Artificial Intelligence, pp. 188\u2013195. Springer, Berlin (2010)"},{"key":"9325_CR50","first-page":"259","volume-title":"Proceedings of the 39th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL)","author":"K Hoder","year":"2012","unstructured":"Hoder, K., Kov\u00e0cs, L., Voronkov, A.: Playing in the grey area of proofs. In: Hicks, M. (ed.) Proceedings of the 39th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL), pp. 259\u2013272. ACM, New York (2012)"},{"key":"9325_CR51","first-page":"181","volume-title":"Proceedings of the 1st annual international conference on computing and combinatorics (COCOON), volume 959 of Lecture Notes in Computer Science","author":"G Huang","year":"1995","unstructured":"Huang, G.: Constructing Craig interpolation formulas. In: Du, D.-Z., Li, M. (eds.) Proceedings of the 1st Annual International Conference on Computing and Combinatorics (COCOON), volume 959 of Lecture Notes in Computer Science, pp. 181\u2013190. Springer, Berlin (1995)"},{"key":"9325_CR52","unstructured":"Jain, H.: Verification using satisfiability checking, predicate abstraction and Craig interpolation. PhD thesis, School of Computer Science, Carnegie Mellon University (2008)"},{"key":"9325_CR53","doi-asserted-by":"crossref","unstructured":"Kapur, D., Majumdar, R., Zarba, C.G., et al.: Interpolation for data structures. In: Devambu, P. (ed.) Proceedings of the 14th ACM SIGSOFT Symposium on the Foundations of Software Engineering. ACM Press (2006)","DOI":"10.1145\/1181775.1181789"},{"key":"9325_CR54","volume-title":"Mathematical logic","author":"SC Kleene","year":"1967","unstructured":"Kleene, S.C.: Mathematical logic. Wiley Interscience, New York (1967)"},{"key":"9325_CR55","first-page":"199","volume-title":"Proceedings of the 22nd Conference on Automated Deduction (CADE), volume 5663 of Lecture Notes in Artificial Intelligence","author":"L Kov\u00e0cs","year":"2009","unstructured":"Kov\u00e0cs, L., Voronkov, A.: Interpolation and symbol elimination. In: Schmidt, R. (ed.) Proceedings of the 22nd Conference on Automated Deduction (CADE), volume 5663 of Lecture Notes in Artificial Intelligence, pp. 199\u2013213. Springer, Berlin (2009)"},{"issue":"2","key":"9325_CR56","doi-asserted-by":"crossref","first-page":"457","DOI":"10.2307\/2275541","volume":"62","author":"J Kraj\u00ed\u010dek","year":"1997","unstructured":"Kraj\u00ed\u010dek, J.: Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic. J. Symb. Log. 62(2), 457\u2013486 (1997)","journal-title":"J. Symb. Log."},{"key":"9325_CR57","doi-asserted-by":"crossref","first-page":"82","DOI":"10.1006\/inco.1997.2674","volume":"140","author":"J Kraj\u00ed\u010dek","year":"1998","unstructured":"Kraj\u00ed\u010dek, J., Pudl\u00e0k, P.: Some consequences of cryptographical conjectures for s 2 1 ${s^{1}_{2}}$ and EF. Inf. Comput. 140, 82\u201394 (1998)","journal-title":"Inf. Comput."},{"key":"9325_CR58","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1109\/FAMCAD.2007.13","volume-title":"Proceedings of the 7th conference on formal methods in computer aided design (FMCAD)","author":"D Kroening","year":"2007","unstructured":"Kroening, D., Weissenbacher, G.: Lifting propositional interpolants to the word-level. In: Baumgartner, J., Sheeran, M. (eds.) Proceedings of the 7th Conference on Formal Methods in Computer Aided Design (FMCAD), pp. 85\u201389. ACM and IEEE, New York (2007)"},{"key":"9325_CR59","first-page":"573","volume-title":"Proceedings of the 23rd conference on computer aided verification (CAV), volume 6806 of Lecture Notes in Computer Science","author":"D Kroening","year":"2011","unstructured":"Kroening, D., Weissenbacher, G.: Interpolation-based software verification with Wolverine. In: Gopalakrishnan, G., Qaader, S. (eds.) Proceedings of the 23rd Conference on Computer Aided Verification (CAV), volume 6806 of Lecture Notes in Computer Science, pp. 573\u2013578. Springer, Berlin (2011)"},{"key":"9325_CR60","first-page":"348","volume-title":"Proceedings of the 14th Conference on Logic, Programming and Automated Reasoning (LPAR), volume 4790 of Lecture Notes in Artificial Intelligence","author":"M Ludwig","year":"2007","unstructured":"Ludwig, M., Waldmann, U.: An extension of the Knuth-Bendix ordering with LPO-like properties. In: Dershowitz, N., Voronkov, A. (eds.) Proceedings of the 14th Conference on Logic, Programming and Automated Reasoning (LPAR), volume 4790 of Lecture Notes in Artificial Intelligence, pp. 348\u2013362. Springer, Berlin (2007)"},{"issue":"8","key":"9325_CR61","doi-asserted-by":"crossref","first-page":"76","DOI":"10.1145\/1536616.1536637","volume":"52","author":"S Malik","year":"2009","unstructured":"Malik, S., Zhang, L.: Boolean satisfiability: from theoretical hardness to practical success. Comm. ACM 52(8), 76\u201382 (2009)","journal-title":"Comm. ACM"},{"key":"9325_CR62","doi-asserted-by":"crossref","unstructured":"Marques-Silva, J.P., Sakallah, K.A.: GRASP: A new search algorithm for satisfiability. In: Proceedings of the 1996 IEEE\/ACM International Conference on Computer Aided Design (ICCAD), pp. 220\u2013227 (1997)","DOI":"10.1109\/ICCAD.1996.569607"},{"issue":"2","key":"9325_CR63","doi-asserted-by":"crossref","first-page":"284","DOI":"10.1145\/151261.151265","volume":"40","author":"D McAllester","year":"1993","unstructured":"McAllester, D.: Automatic recognition of tractability in inference relations. J. ACM 40(2), 284\u2013303 (1993)","journal-title":"J. ACM"},{"key":"9325_CR64","first-page":"1","volume-title":"Interpolation and SAT-based model checking. In: Proceedings of the 15th Conference on Computer Aided Verification (CAV), volume 2725 of Lecture Notes in Computer Science","author":"KL McMillan","year":"2003","unstructured":"McMillan, K.L.: Interpolation and SAT-based model checking. In: Proceedings of the 15th Conference on Computer Aided Verification (CAV), volume 2725 of Lecture Notes in Computer Science, pp. 1\u201313. Springer, Berlin (2003)"},{"issue":"1","key":"9325_CR65","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1016\/j.tcs.2005.07.003","volume":"345","author":"KL McMillan","year":"2005","unstructured":"McMillan, K.L.: An interpolating theorem prover. Theor. Comput. Sci. 345(1), 101\u2013121 (2005)","journal-title":"Theor. Comput. Sci."},{"key":"9325_CR66","first-page":"123","volume-title":"Proceedings of the 18th Conference on Computer Aided Verification (CAV), volume 4144 of Lecture Notes in Computer Science","author":"KL McMillan","year":"2006","unstructured":"McMillan, K.L.: Lazy abstraction with interpolants. In: Ball, T., Jones, R. B. (eds.) Proceedings of the 18th Conference on Computer Aided Verification (CAV), volume 4144 of Lecture Notes in Computer Science, pp. 123\u2013136. Springer, Berlin (2006)"},{"key":"9325_CR67","first-page":"413","volume-title":"Proceedings of the 14th Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS), volume 4963 of Lecture Notes in Computer Science","author":"KL McMillan","year":"2008","unstructured":"McMillan, K.L.: Quantified invariant generation using an interpolating saturation prover. In: Ramakrishnan, C. R., Rehof, J. (eds.) Proceedings of the 14th Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS), volume 4963 of Lecture Notes in Computer Science, pp. 413\u2013427. Springer, Berlin (2008)"},{"key":"9325_CR68","first-page":"104","volume-title":"Lazy annotation for program testing and verification. In: Proceedings of the 22nd Conference on Computer Aided Verification (CAV), volume 6174 of Lecture Notes in Computer Science","author":"KL McMillan","year":"2010","unstructured":"McMillan, K.L.: Lazy annotation for program testing and verification. In: Proceedings of the 22nd Conference on Computer Aided Verification (CAV), volume 6174 of Lecture Notes in Computer Science, pp. 104\u2013118. Springer, Berlin (2010)"},{"key":"9325_CR69","volume-title":"Proceedings of the 11th conference on formal methods in computer aided design (FMCAD)","author":"KL McMillan","year":"2011","unstructured":"McMillan, K.L.: Interpolants from Z3 proofs. In: Bjesse, P., Slobodova, A. (eds.) Proceedings of the 11th Conference on Formal Methods in Computer Aided Design (FMCAD). ACM and IEEE, New York (2011)"},{"key":"9325_CR70","unstructured":"Moska\u0142, M.: Fx7 or in software, it is all about quantifiers. System Descriptions at the Satisfiability Modulo Theories Competition (SMT-COMP) (2007). Available at http:\/\/research.microsoft.com\/en-us\/um\/people\/moskal\/"},{"key":"9325_CR71","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Blaauw, D., Lavagno, L. (eds.) Proceedings of the 39th Design Automation Conference (DAC), pp. 530\u2013535 (2001)","DOI":"10.1145\/378239.379017"},{"key":"9325_CR72","doi-asserted-by":"crossref","first-page":"261","DOI":"10.3233\/FI-1982-53-403","volume":"5","author":"D Mundici","year":"1982","unstructured":"Mundici, D.: Complexity of Craig\u2019s interpolation. Fundamenta Informaticae 5, 261\u2013278 (1982)","journal-title":"Fundamenta Informaticae"},{"key":"9325_CR73","unstructured":"Nelson, G.: Techniques for Program Verification. PhD thesis, Stanford University, 1979. A revised version was published as Xerox PARC Computer Science Laboratory Research Report No. CSL-81-10"},{"key":"9325_CR74","doi-asserted-by":"crossref","unstructured":"Nelson, G.: Combining satisfiability procedures by equality sharing. In: Bledsoe, W. W., Loveland, D. W. (eds.) Automatic Theorem Proving: After 25 Years, pp. 201\u2013211. American Mathematical Society (1983)","DOI":"10.1090\/conm\/029\/11"},{"issue":"2","key":"9325_CR75","doi-asserted-by":"crossref","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G Nelson","year":"1979","unstructured":"Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Trans. Program. Lang. Syst. 1(2), 245\u2013257 (1979)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"6","key":"9325_CR76","doi-asserted-by":"crossref","first-page":"937","DOI":"10.1145\/1217856.1217859","volume":"53","author":"R Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: from an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). J. ACM 53(6), 937\u2013977 (2006)","journal-title":"J. ACM"},{"issue":"3","key":"9325_CR77","doi-asserted-by":"crossref","first-page":"981","DOI":"10.2307\/2275583","volume":"62","author":"P Pudl\u00e0k","year":"1997","unstructured":"Pudl\u00e0k, P.: Lower bounds for resolution and cutting plane proofs and monotone computations. J. Symbolic Logic 62(3), 981\u2013998 (1997)","journal-title":"J. Symbolic Logic"},{"key":"9325_CR78","first-page":"193","volume-title":"Proceedings of the 24th Conference on Computer Aided Verification (CAV), volume 7358 of Lecture Notes in Computer Science","author":"SF Rollini","year":"2012","unstructured":"Rollini, S.F., Sery, O., Sharygina, N.: Leveraging interpolant strength in model checking. In: Parthasarathy, M., Seshia, S. A. (eds.) Proceedings of the 24th Conference on Computer Aided Verification (CAV), volume 7358 of Lecture Notes in Computer Science, pp. 193\u2013209. Springer, Berlin (2012)"},{"key":"9325_CR79","first-page":"347","volume-title":"Proceedings of the 25th Conference on Computer Aided Verification (CAV), volume 8044 of Lecture Notes in Computer Science","author":"P R\u00fcmmer","year":"2013","unstructured":"R\u00fcmmer, P., Hojjat, H., Kuncak, V.: Disjunctive interpolation for Horn clause verification. In: Sharygina, N., Veith, H. (eds.) Proceedings of the 25th Conference on Computer Aided Verification (CAV), volume 8044 of Lecture Notes in Computer Science, pp. 347\u2013363. Springer, Berlin (2013)"},{"key":"9325_CR80","doi-asserted-by":"crossref","unstructured":"R\u00fcmmer, P., Suboti\u0107, P.: Exploring interpolants. In: Jobstmann, B., Ray, S. (eds.) Proceedings of the 13th Conference on Formal Methods in Computer Aided Design (FMCAD). FMCAD Inc (2013)","DOI":"10.1109\/FMCAD.2013.6679393"},{"issue":"4","key":"9325_CR81","doi-asserted-by":"crossref","first-page":"40","DOI":"10.1145\/1592434.1592437","volume":"41","author":"N Shankar","year":"2009","unstructured":"Shankar, N.: Automated deduction for verification. ACM Comput. Surv. 41(4), 40\u201396 (2009)","journal-title":"ACM Comput. Surv."},{"key":"9325_CR82","doi-asserted-by":"crossref","unstructured":"Smullyan, R.M.: First-order logic. Dover Publications, New York (1995). First published by Springer in 1968","DOI":"10.1007\/978-3-642-86718-7"},{"issue":"4","key":"9325_CR83","doi-asserted-by":"crossref","first-page":"Article 1","DOI":"10.2168\/LMCS-4(4:1)2008","volume":"4","author":"V Sofronie-Stokkermans","year":"2008","unstructured":"Sofronie-Stokkermans, V.: Interpolation in local theory extensions. Logical Methods in Computer Science 4(4), Article 1 (2008)","journal-title":"Logical Methods in Computer Science"},{"key":"9325_CR84","volume-title":"Proof theory, volume 81 of studies in logic","author":"G Takeuti","year":"1975","unstructured":"Takeuti, G.: Proof theory, volume 81 of studies in logic. North Holland, Amsterdam (1975)"},{"key":"9325_CR85","doi-asserted-by":"crossref","first-page":"425","DOI":"10.2178\/bsl\/1203350879","volume":"1","author":"A Urquhart","year":"1995","unstructured":"Urquhart, A.: The complexity of propositional proofs. Bull. Symb. Log. 1, 425\u2013467 (1995)","journal-title":"Bull. Symb. Log."},{"key":"9325_CR86","unstructured":"Weissenbacher, G.: Program Analysis with Interpolants. PhD thesis, Magdalen College, Oxford University (2010)"},{"key":"9325_CR87","unstructured":"Yorsh, G., Musuvathi, M.: A combination method for generating interpolants. Technical Report MSR-TR-2004-108, Microsoft Research (2004)"},{"key":"9325_CR88","first-page":"353","volume-title":"Proceedings of the 20th Conference on Automated Deduction (CADE), volume 3632 of Lecture Notes in Artificial Intelligence","author":"G Yorsh","year":"2005","unstructured":"Yorsh, G., Musuvathi, M.: A combination method for generating interpolants. In: Nieuwenhuis, R. (ed.) Proceedings of the 20th Conference on Automated Deduction (CADE), volume 3632 of Lecture Notes in Artificial Intelligence, pp. 353\u2013368. Springer, Berlin (2005)"},{"key":"9325_CR89","first-page":"10880","volume-title":"Validating SAT solvers using an independent resolution-based checker: practical implementations and other applications. In: Proceedings of the Conference on Design Automation and Test in Europe (DATE)","author":"L Zhang","year":"2003","unstructured":"Zhang, L., Malik, S.: Validating SAT solvers using an independent resolution-based checker: practical implementations and other applications. In: Proceedings of the Conference on Design Automation and Test in Europe (DATE), pp. 10880\u201310885. IEEE, Los Alamitos (2003)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-015-9325-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-015-9325-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-015-9325-5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,21]],"date-time":"2025-05-21T03:05:25Z","timestamp":1747796725000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-015-9325-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,3,20]]},"references-count":89,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2015,4]]}},"alternative-id":["9325"],"URL":"https:\/\/doi.org\/10.1007\/s10817-015-9325-5","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,3,20]]}}}