{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T19:25:34Z","timestamp":1725909934267},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319661667"},{"type":"electronic","value":"9783319661674"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-66167-4_18","type":"book-chapter","created":{"date-parts":[[2017,8,28]],"date-time":"2017-08-28T07:15:18Z","timestamp":1503904518000},"page":"316-332","source":"Crossref","is-referenced-by-count":9,"title":["Interpolation, Amalgamation and Combination (The Non-disjoint Signatures Case)"],"prefix":"10.1007","author":[{"given":"Silvio","family":"Ghilardi","sequence":"first","affiliation":[]},{"given":"Alessandro","family":"Gianola","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,8,29]]},"reference":[{"key":"18_CR1","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1007\/BF02485230","volume":"5","author":"PD Bacsich","year":"1975","unstructured":"Bacsich, P.D.: Amalgamation properties and interpolation theorems for equational theories. Algebra Universalis 5, 45\u201355 (1975)","journal-title":"Algebra Universalis"},{"key":"18_CR2","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"118","DOI":"10.1007\/978-3-642-31365-3_12","volume-title":"Automated Reasoning","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.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 118\u2013133. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-31365-3_12"},{"key":"18_CR3","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), 5:1\u20135:34 (2014)","DOI":"10.1145\/2490253"},{"key":"18_CR4","volume-title":"Model Theory","author":"C-C Chang","year":"1990","unstructured":"Chang, C.-C., Keisler, J.H.: Model Theory, 3rd edn. North-Holland, Amsterdam-London (1990)","edition":"3"},{"key":"18_CR5","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, 269\u2013285 (1957)","journal-title":"J. Symb. Log."},{"issue":"3\u20134","key":"18_CR6","doi-asserted-by":"crossref","first-page":"221","DOI":"10.1007\/s10817-004-6241-5","volume":"33","author":"S Ghilardi","year":"2004","unstructured":"Ghilardi, S.: Model theoretic methods in combined constraint satisfiability. J. Autom. Reasoning 33(3\u20134), 221\u2013249 (2004)","journal-title":"J. Autom. Reasoning"},{"key":"18_CR7","doi-asserted-by":"crossref","unstructured":"Ghilardi, S., Gianola, A.: Interpolation, amalgamation and combination (extended version). Technical report (2017)","DOI":"10.1007\/978-3-319-66167-4_18"},{"issue":"3","key":"18_CR8","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1002\/malq.19900360303","volume":"36","author":"S Ghilardi","year":"1990","unstructured":"Ghilardi, S., Meloni, G.C.: Modal logics with $$n$$ -ary connectives. Z. Math. Logik Grundlag. Math. 36(3), 193\u2013215 (1990)","journal-title":"Z. Math. Logik Grundlag. Math."},{"issue":"2","key":"18_CR9","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1342991.1342992","volume":"9","author":"S Ghilardi","year":"2008","unstructured":"Ghilardi, S., Nicolini, E., Zucchelli, D.: A comprehensive framework for combined decision procedures. ACM Trans. Comput. Logic 9(2), 1\u201354 (2008)","journal-title":"ACM Trans. Comput. Logic"},{"key":"18_CR10","doi-asserted-by":"crossref","unstructured":"Henzinger, T., McMillan, K.L., Jhala, R., Majumdar, R.: Abstractions from Proofs. In: POPL, pp. 232\u2013244 (2004)","DOI":"10.1145\/964001.964021"},{"key":"18_CR11","doi-asserted-by":"crossref","unstructured":"Kapur, D., Majumdar, R., Zarba, C.: Interpolation for data structures. In: SIGSOFT\u201906\/FSE-14, pp. 105\u2013116 (2006)","DOI":"10.1145\/1181775.1181789"},{"key":"18_CR12","doi-asserted-by":"crossref","unstructured":"Maksimova, L.L.: Craig\u2019s theorem in superintuitionistic logics and amalgamable varieties. Algebra i Logika 16(6), 643\u2013681, 741 (1977)","DOI":"10.1007\/BF01670006"},{"key":"18_CR13","doi-asserted-by":"crossref","unstructured":"Maksimova, L.L.: Interpolation theorems in modal logics and amalgamable varieties of topological Boolean algebras. Algebra i Logika 18(5), 556\u2013586, 632 (1979)","DOI":"10.1007\/BF01673502"},{"key":"18_CR14","doi-asserted-by":"crossref","unstructured":"Maksimova, L.L.: Interpolation theorems in modal logics. Sufficient conditions. Algebra i Logika 19(2), 194\u2013213, 250\u2013251 (1980)","DOI":"10.1007\/BF01669837"},{"key":"18_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/978-3-540-30124-0_3","volume-title":"Computer Science Logic","author":"K McMillan","year":"2004","unstructured":"McMillan, K.: Applications of craig interpolation to model checking. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004. LNCS, vol. 3210, pp. 22\u201323. Springer, Heidelberg (2004). doi: 10.1007\/978-3-540-30124-0_3"},{"issue":"2","key":"18_CR16","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. Programm. Lang. Syst. 1(2), 245\u2013257 (1979)","journal-title":"ACM Trans. Programm. Lang. Syst."},{"key":"18_CR17","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1007\/978-3-642-02959-2_4","volume-title":"Automated Deduction \u2013 CADE-22","author":"E Nicolini","year":"2009","unstructured":"Nicolini, E., Ringeissen, C., Rusinowitch, M.: Combinable extensions of abelian groups. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol. 5663, pp. 51\u201366. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-02959-2_4"},{"key":"18_CR18","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/978-3-642-04222-5_20","volume-title":"Frontiers of Combining Systems","author":"E Nicolini","year":"2009","unstructured":"Nicolini, E., Ringeissen, C., Rusinowitch, M.: Data structures with arithmetic constraints: a non-disjoint combination. In: Ghilardi, S., Sebastiani, R. (eds.) FroCoS 2009. LNCS (LNAI), vol. 5749, pp. 319\u2013334. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-04222-5_20"},{"key":"18_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"428","DOI":"10.1007\/978-3-642-00768-2_35","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Nicolini","year":"2009","unstructured":"Nicolini, E., Ringeissen, C., Rusinowitch, M.: Satisfiability procedures for combination of theories sharing integer offsets. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 428\u2013442. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-00768-2_35"},{"issue":"1\u20132","key":"18_CR20","doi-asserted-by":"crossref","first-page":"163","DOI":"10.3233\/FI-2010-362","volume":"105","author":"E Nicolini","year":"2010","unstructured":"Nicolini, E., Ringeissen, C., Rusinowitch, M.: Combining satisfiability procedures for unions of theories with a shared counting operator. Fundam. Inform. 105(1\u20132), 163\u2013187 (2010)","journal-title":"Fundam. Inform."},{"key":"18_CR21","unstructured":"Segerberg, K.: An Essay in Classical Modal Logic, Filosofiska Studier, vol. 13. Uppsala Universitet (1971)"},{"issue":"4","key":"18_CR22","doi-asserted-by":"crossref","first-page":"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 Comput. Sci. 4(4), 1\u201331 (2008)","journal-title":"Logical Methods Comput. Sci."},{"key":"18_CR23","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1007\/978-3-319-40229-1_19","volume-title":"Automated Reasoning","author":"V Sofronie-Stokkermans","year":"2016","unstructured":"Sofronie-Stokkermans, V.: On interpolation and symbol elimination in theory extensions. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS (LNAI), vol. 9706, pp. 273\u2013289. Springer, Cham (2016). doi: 10.1007\/978-3-319-40229-1_19"},{"key":"18_CR24","doi-asserted-by":"crossref","unstructured":"Tinelli, C., Harandi, M.T.: A new correctness proof of the Nelson-Oppen combination procedure. In: Proceedings of FroCoS 1996, Applied Logic, pp. 103\u2013120. Kluwer Academic Publishers (1996)","DOI":"10.1007\/978-94-009-0349-4_5"},{"issue":"1","key":"18_CR25","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1007\/s10817-016-9371-7","volume":"57","author":"N Totla","year":"2016","unstructured":"Totla, N., Wies, T.: Complete instantiation-based interpolation. J. Autom. Reasoning 57(1), 37\u201365 (2016)","journal-title":"J. Autom. Reasoning"},{"key":"18_CR26","unstructured":"Wolter, F.: Fusions of modal logics revisited. In Advances in Modal Logic, vol. 1 (Berlin, 1996), CSLI Lecture Notes, pp. 361\u2013379 (1998)"},{"key":"18_CR27","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. 3632, pp. 353\u2013368. Springer, Heidelberg (2005). doi: 10.1007\/11532231_26"}],"container-title":["Lecture Notes in Computer Science","Frontiers of Combining Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-66167-4_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,10,16]],"date-time":"2020-10-16T07:34:40Z","timestamp":1602833680000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-66167-4_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319661667","9783319661674"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66167-4_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}