{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T07:25:13Z","timestamp":1743060313529,"version":"3.40.3"},"publisher-location":"Cham","reference-count":22,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319242453"},{"type":"electronic","value":"9783319242460"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-24246-0_17","type":"book-chapter","created":{"date-parts":[[2015,9,19]],"date-time":"2015-09-19T04:20:53Z","timestamp":1442636453000},"page":"275-290","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["A Rewriting Approach to the Combination of Data Structures with Bridging Theories"],"prefix":"10.1007","author":[{"given":"Paula","family":"Chocron","sequence":"first","affiliation":[]},{"given":"Pascal","family":"Fontaine","sequence":"additional","affiliation":[]},{"given":"Christophe","family":"Ringeissen","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,11,12]]},"reference":[{"key":"17_CR1","doi-asserted-by":"crossref","unstructured":"Armando, A., Bonacina, M.P., Ranise, S., Schulz, S.: New results on rewrite-based satisfiability procedures. ACM Trans. Comput. Log.\u00a010(1) (2009)","DOI":"10.1145\/1459010.1459014"},{"issue":"2","key":"17_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.\u00a0183(2), 140\u2013164 (2003)","journal-title":"Inf. Comput."},{"issue":"2","key":"17_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.\u00a072(2), 535\u2013583 (2007)","journal-title":"J. Symb. Log."},{"key":"17_CR4","doi-asserted-by":"crossref","unstructured":"Baader, F., Nipkow, T.: Term rewriting and all that. Cambridge University Press (1998)","DOI":"10.1017\/CBO9781139172752"},{"issue":"3","key":"17_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.\u00a04(3), 217\u2013247 (1994)","journal-title":"J. Log. Comput."},{"issue":"1\u20132","key":"17_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\u00a03(1\u20132), 21\u201346 (2007)","journal-title":"JSAT"},{"key":"17_CR7","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.\u00a07898, pp. 39\u201357. Springer, Heidelberg (2013)"},{"key":"17_CR8","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.\u00a08562, pp. 122\u2013136. Springer, Heidelberg (2014)"},{"key":"17_CR9","series-title":"LNCS","first-page":"419","volume-title":"CADE 2015","author":"P. Chocron","year":"2015","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.) CADE 2015. LNCS, vol.\u00a09195, pp. 419\u2013433. Springer, Heidelberg (2015)"},{"key":"17_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/978-3-642-04222-5_16","volume-title":"Frontiers of Combining Systems","author":"P. Fontaine","year":"2009","unstructured":"Fontaine, P.: Combinations of theories for decidable fragments of first-order logic. In: Ghilardi, S., Sebastiani, R. (eds.) FroCoS 2009. LNCS, vol.\u00a05749, pp. 263\u2013278. Springer, Heidelberg (2009)"},{"issue":"3-4","key":"17_CR11","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. Journal of Automated Reasoning\u00a033(3-4), 221\u2013249 (2004)","journal-title":"Journal of Automated Reasoning"},{"key":"17_CR12","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., Voronkov, A. (eds.) LPAR-17. LNCS, vol.\u00a06397, pp. 402\u2013416. Springer, Heidelberg (2010)"},{"key":"17_CR13","doi-asserted-by":"crossref","unstructured":"Nicolini, E., Ringeissen, C., Rusinowitch, M.: Combinable extensions of abelian groups. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol.\u00a05663, pp. 51\u201366. Springer, Heidelberg (2009)","DOI":"10.1007\/978-3-642-02959-2_4"},{"issue":"1\u20132","key":"17_CR14","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.\u00a0105(1\u20132), 163\u2013187 (2010)","journal-title":"Fundam. Inform."},{"key":"17_CR15","series-title":"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.\u00a03717, pp. 48\u201364. Springer, Heidelberg (2005)"},{"key":"17_CR16","doi-asserted-by":"crossref","unstructured":"Sofronie-Stokkermans, V.: Locality results for certain extensions of theories with bridging functions. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol.\u00a05663, pp. 67\u201383. Springer, Heidelberg (2009)","DOI":"10.1007\/978-3-642-02959-2_5"},{"key":"17_CR17","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":"17_CR18","doi-asserted-by":"crossref","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 (2010)","DOI":"10.1145\/1707801.1706325"},{"issue":"1","key":"17_CR19","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. Theoretical Comput. Sci.\u00a0290(1), 291\u2013353 (2003)","journal-title":"Theoretical Comput. Sci."},{"issue":"3","key":"17_CR20","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/s10817-005-5204-9","volume":"34","author":"C. Tinelli","year":"2005","unstructured":"Tinelli, C., Zarba, C.G.: Combining non-stably infinite theories. Journal of Automated Reasoning\u00a034(3), 209\u2013238 (2005)","journal-title":"Journal of Automated Reasoning"},{"issue":"2","key":"17_CR21","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.\u00a045(2), 261\u2013286 (2010)","journal-title":"J. Symb. Comput."},{"issue":"10","key":"17_CR22","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.\u00a0204(10), 1526\u20131574 (2006)","journal-title":"Inf. Comput."}],"container-title":["Lecture Notes in Computer Science","Frontiers of Combining Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-24246-0_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,9,8]],"date-time":"2020-09-08T13:32:01Z","timestamp":1599571921000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-24246-0_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319242453","9783319242460"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-24246-0_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"12 November 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}