{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T18:21:07Z","timestamp":1747592467032},"reference-count":61,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2014,10,19]],"date-time":"2014-10-19T00:00:00Z","timestamp":1413676800000},"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,1]]},"DOI":"10.1007\/s10817-014-9314-0","type":"journal-article","created":{"date-parts":[[2014,10,18]],"date-time":"2014-10-18T15:17:06Z","timestamp":1413645426000},"page":"69-97","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":14,"title":["On Interpolation in Automated Theorem Proving"],"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":[[2014,10,19]]},"reference":[{"issue":"3","key":"9314_CR1","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1023\/A:1004275029985","volume":"27","author":"H Andr\u00e9ka","year":"1998","unstructured":"Andr\u00e9ka, H., van Benthem, J., Nemeti, I.: Modal logics and bounded fragments of predicate logic. J. Philos. Log. 27(3), 217\u2013274 (1998)","journal-title":"J. Philos. Log."},{"issue":"1","key":"9314_CR2","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":"9314_CR3","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":"9314_CR4","volume-title":"Methods of Cut-Elimination","author":"M Baaz","year":"2011","unstructured":"Baaz, M., Leitsch, A.: Methods of Cut-Elimination. Springer, Berlin (2011)"},{"key":"9314_CR5","doi-asserted-by":"crossref","unstructured":"B\u00f6hme, S., Moska\u0142, M.: Heaps and data structures: a challenge for automated provers. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) Proceedings of the 23rd Conference on Automated Deduction (CADE), volume 6803 of Lecture Notes in Artificial Intelligence, pp. 177\u2013191. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-22438-6_15"},{"key":"9314_CR6","doi-asserted-by":"crossref","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)","DOI":"10.1145\/1836089.1836090"},{"key":"9314_CR7","unstructured":"Bonacina, M.P.: Two-stage interpolation systems. In: Kov\u00e0cs, L., Weissenbacher, G. (eds.) Notes of the First International Workshop on Interpolation: from Proofs to Applications (IPrA), Twenty-Fifth International Conference on Computer Aided Verification (CAV), Technical Reports. Technische Universit\u00e4t Wien (2013)"},{"key":"9314_CR8","doi-asserted-by":"crossref","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)","DOI":"10.1016\/j.entcs.2006.11.039"},{"issue":"1","key":"9314_CR9","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":"9314_CR10","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":"9314_CR11","doi-asserted-by":"crossref","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)","DOI":"10.1007\/978-3-642-22119-4_1"},{"key":"9314_CR12","unstructured":"Bonacina, M.P., Johansson, M.: Interpolation of ground proofs: a survey. Submitted for publication. Available at http:\/\/profs.sci.univr.it\/bonacina\/ (2014)"},{"key":"9314_CR13","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1007\/s10817-010-9213-y","volume":"47","author":"MP Bonacina","year":"2011","unstructured":"Bonacina, M.P., Lynch, C.A., de Moura, L.: On deciding satisfiability by theorem proving with speculative inferences. J. Autom. Reas. 47, 161\u2013189 (2011)","journal-title":"J. Autom. Reas."},{"key":"9314_CR14","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":"9314_CR15","doi-asserted-by":"crossref","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)","DOI":"10.1007\/978-3-642-31365-3_12"},{"key":"9314_CR16","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"},{"issue":"5\u20136","key":"9314_CR17","doi-asserted-by":"crossref","first-page":"705","DOI":"10.1016\/S0747-7171(06)80010-6","volume":"15","author":"R Chadha","year":"1993","unstructured":"Chadha, R., Plaisted, D.A.: On the mechanical derivation of loop invariants. J. Symb. Comput. 15(5\u20136), 705\u2013744 (1993)","journal-title":"J. Symb. Comput."},{"key":"9314_CR18","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":"9314_CR19","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1145\/1838552.1838559","volume":"12","author":"A Cimatti","year":"2010","unstructured":"Cimatti, A., Griggio, A., Sebastiani, R.: Efficient interpolant generation in satisfiability modulo theory. ACM Trans. Comput. Log. 12(1), 7 (2010)","journal-title":"ACM Trans. Comput. Log."},{"issue":"3","key":"9314_CR20","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":"3","key":"9314_CR21","doi-asserted-by":"crossref","first-page":"269","DOI":"10.2307\/2963594","volume":"22","author":"W Craig","year":"1957","unstructured":"Craig, W.: Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory. J. Symb. Log. 22(3), 269\u2013285 (1957)","journal-title":"J. Symb. Log."},{"key":"9314_CR22","doi-asserted-by":"crossref","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)","DOI":"10.1007\/978-3-540-73595-3_13"},{"key":"9314_CR23","unstructured":"de Moura, L., Bj\u00f8rner, N.: Model-based theory combination. In: Krsti\u0107, S., Oliveras, A. (eds.) Proceedings of the 5th Workshop on Satisfiability Modulo Theories (SMT 2007), volume 198(2) of Electronic Notes in Theoretical Computer Science, pp. 37\u201349. Elsevier, Amsterdam (2008)"},{"key":"9314_CR24","doi-asserted-by":"crossref","unstructured":"de Moura, L., Bj\u00f8rnerc, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Proceedings of the 14th Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 4963 of Lecture Notes in Computer Science, pp. 337\u2013340. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"9314_CR25","doi-asserted-by":"crossref","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)","DOI":"10.1007\/978-3-642-14203-1_34"},{"issue":"9","key":"9314_CR26","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":"9314_CR27","doi-asserted-by":"crossref","unstructured":"Dershowitz, N., Plaisted, D.A.: Rewriting. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. 1, pp. 535\u2013610. Amsterdam, Elsevier (2001)","DOI":"10.1016\/B978-044450813-3\/50011-4"},{"issue":"3","key":"9314_CR28","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. JACM 52(3), 365\u2013473 (2005)","journal-title":"JACM"},{"key":"9314_CR29","unstructured":"Dierkes, M.: Model Building for Sets of Guarded Clauses. PhD thesis, Institut National Polytechnique de Grenoble (2001)"},{"key":"9314_CR30","doi-asserted-by":"crossref","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)","DOI":"10.1007\/978-3-642-11319-2_12"},{"key":"9314_CR31","doi-asserted-by":"crossref","unstructured":"Dutertre, B., de Moura, L.: A fast linear arithmetic solver for DPLL(T). 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. 81\u201394. Springer, Berlin (2006)","DOI":"10.1007\/11817963_11"},{"key":"9314_CR32","unstructured":"Fietzke, A.: Labelled superposition. PhD thesis, Max Planck Institut f\u00fcr Informatik, Saabr\u00fccken (2013)"},{"issue":"4","key":"9314_CR33","doi-asserted-by":"crossref","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":"9314_CR34","doi-asserted-by":"crossref","unstructured":"Fontaine, P.: Combinations of theories for decidable fragments of first-order logic. In: Ghilardi, S., Sebastiani, R. (eds.) Proceedings of the 7th Symposium on Frontiers of Combining Systems (FroCoS), volume 5749 of Lecture Notes in Artificial Intelligence, pp. 263\u2013278. Springer (2009)","DOI":"10.1007\/978-3-642-04222-5_16"},{"key":"9314_CR35","unstructured":"Ganzinger, H., de Nivelle, H.: A superposition decision procedure for the guarded fragment with equality. In: Proceedings of the 14th IEEE Symposium on Logic in Computer Science (LICS). IEEE Computer Society Press (1999)"},{"key":"9314_CR36","doi-asserted-by":"crossref","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)","DOI":"10.1007\/978-3-540-73595-3_12"},{"key":"9314_CR37","doi-asserted-by":"crossref","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)","DOI":"10.1007\/978-3-642-02658-4_25"},{"key":"9314_CR38","doi-asserted-by":"crossref","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)","DOI":"10.1007\/978-3-642-02959-2_16"},{"key":"9314_CR39","doi-asserted-by":"crossref","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)","DOI":"10.1145\/964001.964021"},{"key":"9314_CR40","doi-asserted-by":"crossref","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)","DOI":"10.1007\/978-3-642-14203-1_16"},{"key":"9314_CR41","doi-asserted-by":"crossref","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)","DOI":"10.1145\/2103656.2103689"},{"key":"9314_CR42","doi-asserted-by":"crossref","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)","DOI":"10.1007\/BFb0030832"},{"issue":"3","key":"9314_CR43","doi-asserted-by":"crossref","first-page":"307","DOI":"10.1007\/s11424-006-0307-x","volume":"19","author":"D Kapur","year":"2006","unstructured":"Kapur, D.: A quantifier-elimination based heuristic for automatically generating inductive assertions of programs. J. Syst. Sci. Complexity 19(3), 307\u2013330 (2006)","journal-title":"J. Syst. Sci. Complexity"},{"key":"9314_CR44","doi-asserted-by":"crossref","unstructured":"Kapur, D., Zhang, Z., Horbach, M., Zhao, H., Lu, Q., Nguyen, T.V.: Geometric quantifier elimination heuristics for automatically generating octagonal and max-plus invariants. In: Bonacina, M.P., Stickel, M.E. (eds.) Automated Reasoning and Mathematics: Essays in Memory of William W. McCune, vol. 7788, pp. 189\u2013228. Springer, Berlin (2013)","DOI":"10.1007\/978-3-642-36675-8_11"},{"key":"9314_CR45","doi-asserted-by":"crossref","unstructured":"Kov\u00e0cs, L., Voronkov, A.: Finding loop invariants for programs over arrays using a theorem prover. In: Proc. of the Conf. on Fundamental Approaches to Software Engineering, number 5503 in LNCS, pp. 470\u2013485. Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-00593-0_33"},{"key":"9314_CR46","doi-asserted-by":"crossref","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)","DOI":"10.1007\/978-3-642-02959-2_17"},{"key":"9314_CR47","doi-asserted-by":"crossref","unstructured":"Kov\u00e0cs, L., Voronkov, A.: First order theorem proving and Vampire. 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. 1\u201335. Springer, Berlin (2013)","DOI":"10.1007\/978-3-642-39799-8_1"},{"key":"9314_CR48","doi-asserted-by":"crossref","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)","DOI":"10.1007\/978-3-642-22110-1_45"},{"key":"9314_CR49","doi-asserted-by":"crossref","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)","DOI":"10.1007\/978-3-540-45069-6_1"},{"issue":"1","key":"9314_CR50","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":"9314_CR51","doi-asserted-by":"crossref","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)","DOI":"10.1007\/978-3-540-78800-3_31"},{"key":"9314_CR52","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":"9314_CR53","unstructured":"Moska\u0142, M.: Fx7 or in software, it is all about quantifiers. System Descriptions at the Satisfiability Modulo Theories Competition (SMT-COMP). Available at http:\/\/research.microsoft.com\/en-us\/um\/people\/moskal\/ (2007)"},{"issue":"2","key":"9314_CR54","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":"9314_CR55","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). JACM 53(6), 937\u2013977 (2006)","journal-title":"JACM"},{"key":"9314_CR56","doi-asserted-by":"crossref","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)","DOI":"10.1007\/978-3-642-39799-8_24"},{"key":"9314_CR57","unstructured":"Schulz, S.: System description: E 1.8. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) Proceedings of the 19th Conference on Logic, Programming and Automated Reasoning (LPAR), volume 8312 of Lecture Notes in Artificial Intelligence, pp. 735\u2013743. Springer, Berlin (2013)"},{"issue":"4","key":"9314_CR58","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":"9314_CR59","volume-title":"First-Order Logic","author":"RM Smullyan","year":"1995","unstructured":"Smullyan, R.M.: First-Order Logic. Dover Publications, New York (1995). First published by Springer in 1968"},{"key":"9314_CR60","doi-asserted-by":"crossref","unstructured":"Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: SPASS version 3.5. In: Schmidt, R. (ed.) Proceedings of the 22nd Conference on Automated Deduction (CADE), volume 5663 of Lecture Notes in Artificial Intelligence, pp. 140\u2013145. Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-02959-2_10"},{"key":"9314_CR61","unstructured":"Weissenbacher, G.: Program Analysis with Interpolants. PhD thesis, Magdalen College, Oxford University (2010)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-014-9314-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-014-9314-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-014-9314-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,4,20]],"date-time":"2022-04-20T03:54:11Z","timestamp":1650426851000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-014-9314-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,10,19]]},"references-count":61,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2015,1]]}},"alternative-id":["9314"],"URL":"https:\/\/doi.org\/10.1007\/s10817-014-9314-0","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,10,19]]}}}