{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T09:46:05Z","timestamp":1725529565541},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642007675"},{"type":"electronic","value":"9783642007682"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"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":[[2009]]},"DOI":"10.1007\/978-3-642-00768-2_34","type":"book-chapter","created":{"date-parts":[[2009,3,27]],"date-time":"2009-03-27T01:16:10Z","timestamp":1238116570000},"page":"413-427","source":"Crossref","is-referenced-by-count":21,"title":["Ground Interpolation for the Theory of Equality"],"prefix":"10.1007","author":[{"given":"Alexander","family":"Fuchs","sequence":"first","affiliation":[]},{"given":"Amit","family":"Goel","sequence":"additional","affiliation":[]},{"given":"Jim","family":"Grundy","sequence":"additional","affiliation":[]},{"given":"Sava","family":"Krsti\u0107","sequence":"additional","affiliation":[]},{"given":"Cesare","family":"Tinelli","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"34_CR1","unstructured":"Decision Procedure Toolkit (2008), http:\/\/www.sourceforge.net\/projects\/DPT"},{"key":"34_CR2","unstructured":"Barrett, C., Ranise, S., Stump, A., Tinelli, C.: The Satisfiability Modulo Theories Library, SMT-LIB (2008), http:\/\/www.SMT-LIB.org"},{"key":"34_CR3","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.\u00a04963, pp. 397\u2013412. Springer, Heidelberg (2008)"},{"issue":"3","key":"34_CR4","doi-asserted-by":"publisher","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. Journal of Symbolic Logic\u00a022(3), 269\u2013285 (1957)","journal-title":"Journal of Symbolic Logic"},{"issue":"3\u20134","key":"34_CR5","first-page":"221","volume":"33","author":"S. Ghilardi","year":"2005","unstructured":"Ghilardi, S.: Model-theoretic methods in combined constraint satisfiability. Journal of Automated Reasoning\u00a033(3\u20134), 221\u2013249 (2005)","journal-title":"Journal of Automated Reasoning"},{"key":"34_CR6","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1145\/1181775.1181789","volume-title":"SIGSOFT FSE","author":"D. Kapur","year":"2006","unstructured":"Kapur, D., Majumdar, R., Zarba, C.G.: Interpolation for data structures. In: Young, M., Devanbu, P.T. (eds.) SIGSOFT FSE, pp. 105\u2013116. ACM, New York (2006)"},{"key":"34_CR7","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":"K. McMillan","year":"2003","unstructured":"McMillan, K.: 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":"34_CR8","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 Computer Science\u00a0345(1), 101\u2013121 (2005)","journal-title":"Theoretical Computer Science"},{"issue":"2","key":"34_CR9","doi-asserted-by":"publisher","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 Transactions on Programming Languages and Systems\u00a01(2), 245\u2013257 (1979)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"2","key":"34_CR10","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1145\/322186.322198","volume":"27","author":"G. Nelson","year":"1980","unstructured":"Nelson, G., Oppen, D.C.: Fast decision procedures based on congruence closure. Journal of the ACM\u00a027(2), 356\u2013364 (1980)","journal-title":"Journal of the ACM"},{"key":"34_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1007\/978-3-540-32033-3_33","volume-title":"Term Rewriting and Applications","author":"R. Nieuwenhuis","year":"2005","unstructured":"Nieuwenhuis, R., Oliveras, A.: Proof-producing congruence closure. In: Giesl, J. (ed.) RTA 2005. LNCS, vol.\u00a03467, pp. 453\u2013468. Springer, Heidelberg (2005)"},{"key":"34_CR12","doi-asserted-by":"crossref","unstructured":"Pudl\u00e1k, P.: Lower bounds for resolution and cutting planes proofs and monotone computations. Journal of Symbolic Logic\u00a062(3) (1997)","DOI":"10.2307\/2275583"},{"issue":"1","key":"34_CR13","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1023\/A:1022587501759","volume":"30","author":"C. Tinelli","year":"2003","unstructured":"Tinelli, C.: Cooperation of background reasoners in theory reasoning by residue sharing. Journal of Automated Reasoning\u00a030(1), 1\u201331 (2003)","journal-title":"Journal of Automated Reasoning"},{"key":"34_CR14","series-title":"Lecture Notes in Computer Science","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, vol.\u00a03632, pp. 353\u2013368. Springer, Heidelberg (2005)"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-00768-2_34","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,24]],"date-time":"2023-05-24T16:52:02Z","timestamp":1684947122000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-00768-2_34"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642007675","9783642007682"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-00768-2_34","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}