{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,29]],"date-time":"2025-11-29T07:47:27Z","timestamp":1764402447428},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642113185"},{"type":"electronic","value":"9783642113192"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-11319-2_12","type":"book-chapter","created":{"date-parts":[[2010,1,6]],"date-time":"2010-01-06T05:00:05Z","timestamp":1262754005000},"page":"129-145","source":"Crossref","is-referenced-by-count":71,"title":["Interpolant Strength"],"prefix":"10.1007","author":[{"given":"Vijay","family":"D\u2019Silva","sequence":"first","affiliation":[]},{"given":"Daniel","family":"Kroening","sequence":"additional","affiliation":[]},{"given":"Mitra","family":"Purandare","sequence":"additional","affiliation":[]},{"given":"Georg","family":"Weissenbacher","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"3","key":"12_CR1","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1145\/321466.321469","volume":"15","author":"P.B. Andrews","year":"1968","unstructured":"Andrews, P.B.: Resolution with merging. Journal of the ACM\u00a015(3), 367\u2013381 (1968)","journal-title":"Journal of the ACM"},{"key":"12_CR2","doi-asserted-by":"crossref","unstructured":"Bar-Ilan, O., Fuhrmann, O., Hoory, S., Shacham, O., Strichman, O.: Linear-time reductions of resolution proofs. Technical Report IE\/IS-2008-02, Technion (2008)","DOI":"10.1007\/978-3-642-01702-5_14"},{"key":"12_CR3","series-title":"NATO ASI Series F: Computer and Systems Sciences","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1007\/978-3-642-58622-4_5","volume-title":"Computational Logic","author":"S.R. Buss","year":"1999","unstructured":"Buss, S.R.: Propositional proof complexity: An introduction. In: Berger, U., Schwichtenberg, H. (eds.) Computational Logic. NATO ASI Series F: Computer and Systems Sciences, vol.\u00a0165, pp. 127\u2013178. Springer, Heidelberg (1999)"},{"issue":"3","key":"12_CR4","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. Journal of Symbolic Logic\u00a022(3), 250\u2013268 (1957)","journal-title":"Journal of Symbolic Logic"},{"key":"12_CR5","doi-asserted-by":"crossref","unstructured":"D\u2019Silva, V., Kroening, D., Purandare, M., Weissenbacher, G.: Interpolant strength. Technical Report 652, Institute for Computer Science, ETH Zurich (November 2009)","DOI":"10.1007\/978-3-642-11319-2_12"},{"key":"12_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/BFb0030832","volume-title":"Computing and Combinatorics","author":"G. Huang","year":"1995","unstructured":"Huang, G.: Constructing Craig interpolation formulas. In: Li, M., Du, D.-Z. (eds.) COCOON 1995. LNCS, vol.\u00a0959, pp. 181\u2013190. Springer, Heidelberg (1995)"},{"key":"12_CR7","doi-asserted-by":"crossref","unstructured":"Jhala, R., McMillan, K.L.: Interpolant-based transition relation approximation. Logical Methods in Computer Science (LMCS)\u00a03(4) (2007)","DOI":"10.2168\/LMCS-3(4:1)2007"},{"issue":"2","key":"12_CR8","doi-asserted-by":"publisher","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. The Journal of Symbolic Logic\u00a062(2), 457\u2013486 (1997)","journal-title":"The Journal of Symbolic Logic"},{"key":"12_CR9","first-page":"235","volume":"12","author":"S. Maehara","year":"1961","unstructured":"Maehara, S.: On the interpolation theorem of Craig (in Japanese). S\u00fbgaku\u00a012, 235\u2013237 (1961)","journal-title":"S\u00fbgaku"},{"key":"12_CR10","series-title":"Synthese","volume-title":"Interpolations. Essays in Honor of William Craig","author":"P. Mancosu","year":"2008","unstructured":"Mancosu, P.: Interpolations. Essays in Honor of William Craig. Synthese, vol.\u00a0164:3. Springer, Heidelberg (2008)"},{"key":"12_CR11","series-title":"Lecture Notes in Computer Science","first-page":"1","volume-title":"Computer Aided Verification","author":"K.L. McMillan","year":"2003","unstructured":"McMillan, K.L.: Interpolation and SAT-based model checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 1\u201313. Springer, Heidelberg (2003)"},{"issue":"1","key":"12_CR12","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/j.tcs.2005.07.003","volume":"345","author":"K.L. McMillan","year":"2005","unstructured":"McMillan, K.L.: An interpolating theorem prover. Theoretical Comput. Sci.\u00a0345(1), 101\u2013121 (2005)","journal-title":"Theoretical Comput. Sci."},{"issue":"3","key":"12_CR13","doi-asserted-by":"publisher","first-page":"981","DOI":"10.2307\/2275583","volume":"62","author":"P. Pudl\u00e1k","year":"1997","unstructured":"Pudl\u00e1k, P.: Lower bounds for resolution and cutting plane proofs and monotone computations. The Journal of Symbolic Logic\u00a062(3), 981\u2013998 (1997)","journal-title":"The Journal of Symbolic Logic"},{"key":"12_CR14","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","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)"}],"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-11319-2_12.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T02:39:28Z","timestamp":1606185568000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-11319-2_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642113185","9783642113192"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-11319-2_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}