{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:34:44Z","timestamp":1740123284808,"version":"3.37.3"},"reference-count":34,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2019,1,22]],"date-time":"2019-01-22T00:00:00Z","timestamp":1548115200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2020,1]]},"DOI":"10.1007\/s10817-019-09512-4","type":"journal-article","created":{"date-parts":[[2019,1,23]],"date-time":"2019-01-23T21:40:26Z","timestamp":1548279626000},"page":"97-134","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Politeness and Combination Methods for Theories with Bridging Functions"],"prefix":"10.1007","volume":"64","author":[{"given":"Paula","family":"Chocron","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4700-6031","authenticated-orcid":false,"given":"Pascal","family":"Fontaine","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5937-6059","authenticated-orcid":false,"given":"Christophe","family":"Ringeissen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,1,22]]},"reference":[{"issue":"1","key":"9512_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":"9512_CR2","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1016\/S0890-5401(03)00020-8","volume":"183","author":"A Armando","year":"2003","unstructured":"Armando, A., Ranise, S., Rusinowitch, M.: A rewriting approach to satisfiability procedures. Inf. Comput. 183(2), 140\u2013164 (2003)","journal-title":"Inf. Comput."},{"issue":"2","key":"9512_CR3","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":"9512_CR4","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139172752","volume-title":"Term Rewriting and All That","author":"F Baader","year":"1998","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)"},{"issue":"3","key":"9512_CR5","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1093\/logcom\/4.3.217","volume":"4","author":"L Bachmair","year":"1994","unstructured":"Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. J. Log. Comput. 4(3), 217\u2013247 (1994)","journal-title":"J. Log. Comput."},{"issue":"1\u20132","key":"9512_CR6","first-page":"21","volume":"3","author":"C Barrett","year":"2007","unstructured":"Barrett, C., Shikanian, I., Tinelli, C.: An abstract decision procedure for a theory of inductive data types. JSAT 3(1\u20132), 21\u201346 (2007)","journal-title":"JSAT"},{"key":"9512_CR7","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/978-3-642-38574-2_3","volume-title":"Automated Deduction \u2013 CADE-24","author":"Peter Baumgartner","year":"2013","unstructured":"Baumgartner, P., Waldmann, U.: Hierarchic superposition with weak abstraction. In: Bonacina, M.P. (ed.) 24th International Conference on Automated Deduction (CADE-24), Lake Placid, NY, USA, volume 7898 of LNCS, pp. 39\u201357. Springer (2013)"},{"key":"9512_CR8","doi-asserted-by":"crossref","unstructured":"Chocron, P., Fontaine, P., Ringeissen, C.: A Gentle non-disjoint combination of satisfiability procedures. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) Proceedings of the 7th International Joint Conference on Automated Reasoning, IJCAR, volume 8562 of LNCS, pp. 122\u2013136. Springer (2014)","DOI":"10.1007\/978-3-319-08587-6_9"},{"key":"9512_CR9","doi-asserted-by":"crossref","unstructured":"Chocron, P., Fontaine, P., Ringeissen, C.: A polite non-disjoint combination method: theories with bridging functions revisited. In: Felty, A.P., Middeldorp, A. (eds.) 25th International Conference on Automated Deduction (CADE-25), Berlin, Germany, volume 9195 of LNCS, pp. 419\u2013433. Springer (2015)","DOI":"10.1007\/978-3-319-21401-6_29"},{"key":"9512_CR10","doi-asserted-by":"crossref","unstructured":"Chocron, P., Fontaine, P., Ringeissen, C.: A rewriting approach to the combination of data structures with bridging theories. In: Lutz, C., Ranise, S. (eds.) Frontiers of Combining Systems (FroCoS), volume 9322 of LNCS, pp. 275\u2013290. Springer (2015)","DOI":"10.1007\/978-3-319-24246-0_17"},{"key":"9512_CR11","doi-asserted-by":"crossref","unstructured":"Fontaine, P., Ranise, S., Zarba, C.G.: Combining lists with non-stably infinite theories. In Baader, F., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning (LPAR\u201904), volume 3452 of LNCS, pp. 51\u201366. Springer (2005)","DOI":"10.1007\/978-3-540-32275-7_4"},{"issue":"3\u20134","key":"9512_CR12","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. Reason. 33(3\u20134), 221\u2013249 (2004)","journal-title":"J. Autom. Reason."},{"key":"9512_CR13","doi-asserted-by":"crossref","unstructured":"Jovanovic, D., Barrett, C.: Polite theories revisited. In: Fermueller, C., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning (LPAR\u201910), volume 6397 of LNCS, pp. 402\u2013416. Springer (2010)","DOI":"10.1007\/978-3-642-16242-8_29"},{"issue":"4","key":"9512_CR14","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/s11786-012-0135-4","volume":"6","author":"E Kruglov","year":"2012","unstructured":"Kruglov, E., Weidenbach, C.: Superposition decides the first-order logic fragment over ground theories. Math. Comput. Sci. 6(4), 427\u2013456 (2012)","journal-title":"Math. Comput. Sci."},{"issue":"2","key":"9512_CR15","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":"9512_CR16","doi-asserted-by":"crossref","unstructured":"Nicolini, E., Ringeissen, C., Rusinowitch, M.: Combinable extensions of Abelian groups. In: Schmidt, R.A. (ed.) 22nd International Conference on Automated Deduction (CADE-22), Montreal, Canada, volume 5663 of LNCS, pp. 51\u201366. Springer (2009)","DOI":"10.1007\/978-3-642-02959-2_4"},{"issue":"1\u20132","key":"9512_CR17","doi-asserted-by":"publisher","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."},{"issue":"3","key":"9512_CR18","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1145\/322203.322204","volume":"27","author":"DC Oppen","year":"1980","unstructured":"Oppen, D.C.: Reasoning about recursively defined data structures. J. ACM 27(3), 403\u2013411 (1980)","journal-title":"J. ACM"},{"issue":"4","key":"9512_CR19","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/s10817-016-9368-2","volume":"57","author":"T Pham","year":"2016","unstructured":"Pham, T., Gacek, A., Whalen, M.W.: Reasoning about algebraic data types with abstractions. J. Autom. Reason. 57(4), 281\u2013318 (2016)","journal-title":"J. Autom. Reason."},{"key":"9512_CR20","doi-asserted-by":"crossref","unstructured":"Ranise, S., Ringeissen, C., Zarba, C.G.: Combining data structures with nonstably infinite theories using many-sorted logic. In: Gramlich, B. (ed.) Frontiers of Combining Systems (FroCoS), volume 3717 of LNCS, pp. 48\u201364. Springer (2005)","DOI":"10.1007\/11559306_3"},{"issue":"2","key":"9512_CR21","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1145\/322123.322137","volume":"26","author":"RE Shostak","year":"1979","unstructured":"Shostak, R.E.: A practical decision procedure for arithmetic with function symbols. J. ACM 26(2), 351\u2013360 (1979)","journal-title":"J. ACM"},{"key":"9512_CR22","doi-asserted-by":"crossref","unstructured":"Sofronie-Stokkermans, V.: Locality results for certain extensions of theories with bridging functions. In: Schmidt, R.A. (ed.) 22nd International Conference on Automated Deduction (CADE-22), Montreal, Canada, volume 5663 of LNCS, pp. 67\u201383. Springer (2009)","DOI":"10.1007\/978-3-642-02959-2_5"},{"key":"9512_CR23","unstructured":"Sofronie-Stokkermans, V.: Automated reasoning in extensions of theories of constructors with recursively defined functions and homomorphisms. In: Ball, T., Giesl, J., H\u00e4hnle, R., Nipkow, T. (eds.) Interaction versus Automation: The Two Faces of Deduction, number 09411 in Dagstuhl Seminar Proceedings. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Germany (2010)"},{"key":"9512_CR24","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":"9512_CR25","doi-asserted-by":"crossref","unstructured":"Suter, P., K\u00f6ksal, A.S., Kuncak, V.: Satisfiability modulo recursive programs. In: Yahav, E. (ed.) 18th International Symposium on Static Analysis (SAS), Venice, Italy, volume 6887 of LNCS, pp. 298\u2013315. Springer (2011)","DOI":"10.1007\/978-3-642-23702-7_23"},{"issue":"1","key":"9512_CR26","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. J. Autom. Reason. 30(1), 1\u201331 (2003)","journal-title":"J. Autom. Reason."},{"key":"9512_CR27","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/978-94-009-0349-4_5","volume-title":"Frontiers of Combining Systems (FroCoS). Applied Logic","author":"C Tinelli","year":"1996","unstructured":"Tinelli, C., Harandi, M.T.: A new correctness proof of the Nelson\u2013Oppen combination procedure. In: Baader, F., Schulz, K.U. (eds.) Frontiers of Combining Systems (FroCoS). Applied Logic, pp. 103\u2013120. Kluwer Academic Publishers, Dordrecht (1996)"},{"issue":"1","key":"9512_CR28","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. Theor. Comput. Sci. 290(1), 291\u2013353 (2003)","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"9512_CR29","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1016\/j.jsc.2008.10.006","volume":"45","author":"D Tran","year":"2010","unstructured":"Tran, D., Ringeissen, C., Ranise, S., Kirchner, H.: Combination of convex theories: modularity, deduction completeness, and explanation. J. Symb. Comput. 45(2), 261\u2013286 (2010)","journal-title":"J. Symb. Comput."},{"key":"9512_CR30","doi-asserted-by":"crossref","unstructured":"Wies, T., Piskac, R., Kuncak, V.: Combining theories with shared set operations. In: Ghilardi, S., Sebastiani, R. (eds.) Frontiers of Combining Systems (FroCoS), volume 5749 of LNCS, pp. 366\u2013382. Springer (2009)","DOI":"10.1007\/978-3-642-04222-5_23"},{"key":"9512_CR31","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":"9512_CR32","doi-asserted-by":"crossref","unstructured":"Zarba, C.G.: Combining multisets with integers. In: Voronkov, A. (ed.) 18th International Conference on Automated Deduction (CADE-18), Copenhagen, Denmark, volume 2392 of LNCS, pp. 363\u2013376. Springer (2002)","DOI":"10.1007\/3-540-45620-1_30"},{"issue":"1","key":"9512_CR33","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. Reason. 34(1), 1\u201329 (2005)","journal-title":"J. Autom. Reason."},{"issue":"10","key":"9512_CR34","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":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-019-09512-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-019-09512-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-019-09512-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,2,3]],"date-time":"2020-02-03T10:15:01Z","timestamp":1580724901000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-019-09512-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,22]]},"references-count":34,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2020,1]]}},"alternative-id":["9512"],"URL":"https:\/\/doi.org\/10.1007\/s10817-019-09512-4","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2019,1,22]]},"assertion":[{"value":"15 December 2016","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"8 January 2019","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"22 January 2019","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}