{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,20]],"date-time":"2026-06-20T03:53:33Z","timestamp":1781927613655,"version":"3.54.5"},"publisher-location":"Berlin, Heidelberg","reference-count":10,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540371878","type":"print"},{"value":"9783540371885","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11814771_21","type":"book-chapter","created":{"date-parts":[[2006,10,5]],"date-time":"2006-10-05T15:44:21Z","timestamp":1160063061000},"page":"235-250","source":"Crossref","is-referenced-by-count":23,"title":["Interpolation in Local Theory Extensions"],"prefix":"10.1007","author":[{"given":"Viorica","family":"Sofronie-Stokkermans","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"21_CR1","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/BF02485230","volume":"5","author":"P.D. Bacsich","year":"1975","unstructured":"Bacsich, P.D.: Amalgamation properties and interpolation theorem for equational theories. Algebra Universalis\u00a05, 45\u201355 (1975)","journal-title":"Algebra Universalis"},{"key":"21_CR2","first-page":"146","volume-title":"The Theory of Models, Proc. of the 1963 Symposium at Berkeley","author":"B. J\u00f3nsson","year":"1965","unstructured":"J\u00f3nsson, B.: Extensions of relational structures. In: Addison, J.W., Henkin, L., Tarski, A. (eds.) The Theory of Models, Proc. of the 1963 Symposium at Berkeley, pp. 146\u2013157. North-Holland, Amsterdam (1965)"},{"key":"21_CR3","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.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)"},{"key":"21_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/978-3-540-24730-2_2","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K.L. McMillan","year":"2004","unstructured":"McMillan, K.L.: An interpolating theorem prover. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 16\u201330. Springer, Heidelberg (2004)"},{"key":"21_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-31980-1_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K.L. McMillan","year":"2005","unstructured":"McMillan, K.L.: Applications of Craig interpolants in model checking. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 1\u201312. Springer, Heidelberg (2005)"},{"key":"21_CR6","unstructured":"V.\u00a0Sofronie-Stokkermans. On combinations of local theory extensions (Submitted)"},{"key":"21_CR7","unstructured":"Sofronie-Stokkermans, V.: Automated theorem proving by resolution in non-classical logics. In: 4th Int. Conf. Journees de l\u2019Informatique Messine: Knowledge Discovery and Discrete Mathematics (JIM-03), pp. 151\u2013167 (2003)"},{"key":"21_CR8","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/11532231_16","volume-title":"Automated Deduction \u2013 CADE-20","author":"V. Sofronie-Stokkermans","year":"2005","unstructured":"Sofronie-Stokkermans, V.: Hierarchic reasoning in local theory extensions. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol.\u00a03632, pp. 219\u2013234. Springer, Heidelberg (2005)"},{"key":"21_CR9","doi-asserted-by":"crossref","unstructured":"Wro\u0144ski, A.: On a form of equational interpolation property. In: Foundations of logic and linguistics (Salzburg, 1983), Plenum, New York, pp. 23\u201329 (1985)","DOI":"10.1007\/978-1-4899-0548-2_2"},{"key":"21_CR10","series-title":"Lecture Notes in Artificial Intelligence","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 (LNAI), vol.\u00a03632, pp. 353\u2013368. Springer, Heidelberg (2005)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11814771_21.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T07:27:34Z","timestamp":1619508454000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11814771_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540371878","9783540371885"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/11814771_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006]]}}}