{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:29:21Z","timestamp":1767929361585,"version":"3.49.0"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319214009","type":"print"},{"value":"9783319214016","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-21401-6_29","type":"book-chapter","created":{"date-parts":[[2015,7,24]],"date-time":"2015-07-24T10:13:46Z","timestamp":1437732826000},"page":"419-433","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["A Polite Non-Disjoint Combination Method: Theories with Bridging Functions Revisited"],"prefix":"10.1007","author":[{"given":"Paula","family":"Chocron","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pascal","family":"Fontaine","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christophe","family":"Ringeissen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,7,25]]},"reference":[{"issue":"1","key":"29_CR1","doi-asserted-by":"publisher","first-page":"4","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), 4 (2009)","journal-title":"ACM Trans. Comput. Log."},{"issue":"2","key":"29_CR2","doi-asserted-by":"publisher","first-page":"535","DOI":"10.2178\/jsl\/1185803623","volume":"72","author":"F Baader","year":"2007","unstructured":"Baader, F., Ghilardi, S.: Connecting many-sorted theories. J. Symb. Log. 72(2), 535\u2013583 (2007)","journal-title":"J. Symb. Log."},{"key":"29_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/978-3-642-38574-2_3","volume-title":"Automated Deduction \u2013 CADE-24","author":"P Baumgartner","year":"2013","unstructured":"Baumgartner, P., Waldmann, U.: Hierarchic superposition with weak abstraction. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol. 7898, pp. 39\u201357. Springer, Heidelberg (2013)"},{"key":"29_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"122","DOI":"10.1007\/978-3-319-08587-6_9","volume-title":"Automated Reasoning","author":"P Chocron","year":"2014","unstructured":"Chocron, P., Fontaine, P., Ringeissen, C.: A gentle non-disjoint combination of satisfiability procedures. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS, vol. 8562, pp. 122\u2013136. Springer, Heidelberg (2014). http:\/\/hal.inria.fr\/hal-00985135"},{"key":"29_CR5","doi-asserted-by":"crossref","unstructured":"Chocron, P., Fontaine, P., Ringeissen, C.: A Polite Non-Disjoint Combination Method: Theories with Bridging Functions Revisited (Extended Version) (2015). http:\/\/hal.inria.fr","DOI":"10.1007\/978-3-319-21401-6_29"},{"key":"29_CR6","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1007\/978-3-540-32275-7_4","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"P Fontaine","year":"2005","unstructured":"Fontaine, P., Ranise, S., Zarba, C.G.: Combining lists with non-stably infinite theories. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS (LNAI), vol. 3452, pp. 51\u201366. Springer, Heidelberg (2005)"},{"issue":"3\u20134","key":"29_CR7","doi-asserted-by":"publisher","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":"29_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"402","DOI":"10.1007\/978-3-642-16242-8_29","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"D Jovanovi\u0107","year":"2010","unstructured":"Jovanovi\u0107, D., Barrett, C.: Polite theories revisited. In: Ferm\u00fcller, C.G., Voronkov, A. (eds.) LPAR-17. LNCS, vol. 6397, pp. 402\u2013416. Springer, Heidelberg (2010)"},{"issue":"2","key":"29_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 Trans. Program. Lang. Syst. 1(2), 245\u2013257 (1979)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"29_CR10","series-title":"Lecture Notes in Computer Science","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-22. LNCS, vol. 5663, pp. 51\u201366. Springer, Heidelberg (2009)"},{"issue":"1\u20132","key":"29_CR11","first-page":"163","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. Inf. 105(1\u20132), 163\u2013187 (2010)","journal-title":"Fundam. Inf."},{"key":"29_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/978-3-642-54108-7_7","volume-title":"Verified Software: Theories, Tools, Experiments","author":"T-H Pham","year":"2014","unstructured":"Pham, T.-H., Whalen, M.W.: An improved unrolling-based decision procedure for algebraic data types. In: Cohen, E., Rybalchenko, A. (eds.) VSTTE 2013. LNCS, vol. 8164, pp. 129\u2013148. Springer, Heidelberg (2014)"},{"key":"29_CR13","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1007\/11559306_3","volume-title":"Frontiers of Combining Systems","author":"S Ranise","year":"2005","unstructured":"Ranise, S., Ringeissen, C., Zarba, C.G.: Combining data structures with nonstably infinite theories using many-sorted logic. In: Gramlich, B. (ed.) FroCoS 2005. LNCS (LNAI), vol. 3717, pp. 48\u201364. Springer, Heidelberg (2005)"},{"key":"29_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/978-3-642-02959-2_5","volume-title":"Automated Deduction \u2013 CADE-22","author":"V Sofronie-Stokkermans","year":"2009","unstructured":"Sofronie-Stokkermans, V.: Locality results for certain extensions of theories with bridging functions. In: Schmidt, R.A. (ed.) CADE-22. LNCS, vol. 5663, pp. 67\u201383. Springer, Heidelberg (2009)"},{"key":"29_CR15","first-page":"199","volume-title":"Principles of Programming Languages (POPL)","author":"P Suter","year":"2010","unstructured":"Suter, P., Dotta, M., Kuncak, V.: Decision procedures for algebraic data types with abstractions. In: Hermenegildo, M.V., Palsberg, J. (eds.) Principles of Programming Languages (POPL), pp. 199\u2013210. ACM, New York (2010)"},{"key":"29_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/978-3-642-23702-7_23","volume-title":"Static Analysis","author":"P Suter","year":"2011","unstructured":"Suter, P., K\u00f6ksal, A.S., Kuncak, V.: Satisfiability modulo recursive programs. In: Yahav, E. (ed.) Static Analysis. LNCS, vol. 6887, pp. 298\u2013315. Springer, Heidelberg (2011)"},{"key":"29_CR17","doi-asserted-by":"crossref","unstructured":"Tinelli, C., Harandi, M.T.: A new correctness proof of the Nelson-Oppen combination procedure. In: Baader, F., Schulz, K.U. (eds.) Frontiers of Combining Systems (FroCoS), Applied Logic, pp. 103\u2013120. Kluwer Academic Publishers (1996)","DOI":"10.1007\/978-94-009-0349-4_5"},{"issue":"1","key":"29_CR18","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1016\/S0304-3975(01)00332-2","volume":"290","author":"C Tinelli","year":"2003","unstructured":"Tinelli, C., Ringeissen, C.: Unions of non-disjoint theories and combinations of satisfiability procedures. Theoret. Comput. Sci. 290(1), 291\u2013353 (2003)","journal-title":"Theoret. Comput. Sci."},{"key":"29_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1007\/978-3-642-04222-5_23","volume-title":"Frontiers of Combining Systems","author":"T Wies","year":"2009","unstructured":"Wies, T., Piskac, R., Kuncak, V.: Combining theories with shared set operations. In: Ghilardi, S., Sebastiani, R. (eds.) FroCoS 2009. LNCS, vol. 5749, pp. 366\u2013382. Springer, Heidelberg (2009)"},{"key":"29_CR20","unstructured":"Zarba, C.G.: Combining lists with integers. In: International Joint Conference on Automated Reasoning (Short Papers), Technical report DII 11\/01, pp. 170\u2013179. University of Siena (2001)"},{"key":"29_CR21","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/3-540-45620-1_30","volume-title":"Automated Deduction - CADE-18","author":"CG Zarba","year":"2002","unstructured":"Zarba, C.G.: Combining multisets with integers. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 363\u2013376. Springer, Heidelberg (2002)"},{"issue":"1","key":"29_CR22","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10817-005-3075-8","volume":"34","author":"CG Zarba","year":"2005","unstructured":"Zarba, C.G.: Combining sets with cardinals. J. Autom. Reasoning 34(1), 1\u201329 (2005)","journal-title":"J. Autom. Reasoning"},{"issue":"10","key":"29_CR23","doi-asserted-by":"publisher","first-page":"1526","DOI":"10.1016\/j.ic.2006.03.004","volume":"204","author":"T Zhang","year":"2006","unstructured":"Zhang, T., Sipma, H.B., Manna, Z.: Decision procedures for term algebras with integer constraints. Inf. Comput. 204(10), 1526\u20131574 (2006)","journal-title":"Inf. Comput."}],"container-title":["Lecture Notes in Computer Science","Automated Deduction - CADE-25"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-21401-6_29","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,1]],"date-time":"2023-02-01T17:32:22Z","timestamp":1675272742000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-21401-6_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319214009","9783319214016"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-21401-6_29","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"25 July 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}