{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T20:29:25Z","timestamp":1725568165297},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540405597"},{"type":"electronic","value":"9783540450856"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/978-3-540-45085-6_17","type":"book-chapter","created":{"date-parts":[[2010,10,26]],"date-time":"2010-10-26T13:13:30Z","timestamp":1288098810000},"page":"212-227","source":"Crossref","is-referenced-by-count":3,"title":["Matching in a Class of Combined Non-disjoint Theories"],"prefix":"10.1007","author":[{"given":"Christophe","family":"Ringeissen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"2","key":"17_CR1","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1006\/jsco.1996.0009","volume":"21","author":"F. Baader","year":"1996","unstructured":"Baader, F., Schulz, K.U.: Unification in the union of disjoint equational theories: Combining decision procedures. Journal of Symbolic Computation\u00a021(2), 211\u2013243 (1996)","journal-title":"Journal of Symbolic Computation"},{"key":"17_CR2","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1016\/S0304-3975(97)00147-3","volume":"192","author":"F. Baader","year":"1998","unstructured":"Baader, F., Schulz, K.U.: Combination of constraint solvers for free and quasifree structures. Theoretical Computer Science\u00a0192, 107\u2013161 (1998)","journal-title":"Theoretical Computer Science"},{"key":"17_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/3-540-48685-2_14","volume-title":"Rewriting Techniques and Applications","author":"F. Baader","year":"1999","unstructured":"Baader, F., Tinelli, C.: Deciding the word problem in the union of equational theories sharing constructors. In: Narendran, P., Rusinowitch, M. (eds.) RTA 1999. LNCS, vol.\u00a01631, pp. 175\u2013189. Springer, Heidelberg (1999)"},{"key":"17_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/10720084_17","volume-title":"Frontiers of Combining Systems","author":"F. Baader","year":"2000","unstructured":"Baader, F., Tinelli, C.: Combining equational theories sharing non-collapsefree constructors. In: Kirchner, H. (ed.) FroCos 2000. LNCS, vol.\u00a01794, pp. 260\u2013274. Springer, Heidelberg (2000)"},{"key":"17_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"352","DOI":"10.1007\/3-540-45610-4_25","volume-title":"Rewriting Techniques and Applications","author":"F. Baader","year":"2002","unstructured":"Baader, F., Tinelli, C.: Combining decision procedures for positive theories sharing constructors. In: Tison, S. (ed.) RTA 2002. LNCS, vol.\u00a02378, pp. 352\u2013366. Springer, Heidelberg (2002)"},{"issue":"6","key":"17_CR6","doi-asserted-by":"publisher","first-page":"597","DOI":"10.1006\/jsco.1993.1066","volume":"16","author":"A. Boudet","year":"1993","unstructured":"Boudet, A.: Combining unification algorithms. Journal of Symbolic Computation\u00a016(6), 597\u2013626 (1993)","journal-title":"Journal of Symbolic Computation"},{"key":"17_CR7","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1007\/3-540-58156-1_19","volume-title":"Automated Deduction - CADE-12","author":"E. Domenjoud","year":"1994","unstructured":"Domenjoud, E., Klay, F., Ringeissen, C.: Combination techniques for nondisjoint equational theories. In: Bundy, A. (ed.) CADE 1994. LNCS (LNAI), vol.\u00a0814, pp. 267\u2013281. Springer, Heidelberg (1994)"},{"key":"17_CR8","first-page":"257","volume-title":"Computational Logic. Essays in honor of Alan Robinson, ch. 8","author":"J.-P. Jouannaud","year":"1991","unstructured":"Jouannaud, J.-P., Kirchner, C.: Solving equations in abstract algebras: a rulebased survey of unification. In: Lassez, J.-L., Plotkin, G. (eds.) Computational Logic. Essays in honor of Alan Robinson, ch. 8, pp. 257\u2013321. MIT Press, Cambridge (1991)"},{"issue":"2","key":"17_CR9","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1006\/jsco.1994.1040","volume":"18","author":"H. Kirchner","year":"1994","unstructured":"Kirchner, H., Ringeissen, C.: Combining symbolic constraint solvers on algebraic domains. Journal of Symbolic Computation\u00a018(2), 113\u2013155 (1994)","journal-title":"Journal of Symbolic Computation"},{"issue":"2","key":"17_CR10","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. on Programming Languages and Systems\u00a01(2), 245\u2013257 (1979)","journal-title":"ACM Trans. on Programming Languages and Systems"},{"key":"17_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"343","DOI":"10.1007\/3-540-51081-8_118","volume-title":"Proc. Rewriting Techniques and Applications","author":"T. Nipkow","year":"1989","unstructured":"Nipkow, T.: Combining matching algorithms: The regular case. In: Dershowitz, N. (ed.) Proc. Rewriting Techniques and Applications, Chapel Hill, N.C., USA. LNCS, vol.\u00a0335, pp. 343\u2013358. Springer, Heidelberg (1989)"},{"key":"17_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/BFb0013067","volume-title":"Logic Programming and Automated Reasoning","author":"C. Ringeissen","year":"1992","unstructured":"Ringeissen, C.: Unification in a combination of equational theories with shared constants and its application to primal algebras. In: Voronkov, A. (ed.) LPAR 1992. LNCS, vol.\u00a0624, pp. 261\u2013272. Springer, Heidelberg (1992)"},{"issue":"2","key":"17_CR13","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1006\/inco.1996.0042","volume":"126","author":"C. Ringeissen","year":"1996","unstructured":"Ringeissen, C.: Combining decision algorithms for matching in the union of disjoint equational theories. Information and Computation\u00a0126(2), 144\u2013160 (1996)","journal-title":"Information and Computation"},{"doi-asserted-by":"crossref","unstructured":"Ringeissen, C.: Matching and Unification in a Class of Combined Non-Disjoint Theories. INRIA Research Report (2003)","key":"17_CR14","DOI":"10.1007\/978-3-540-45085-6_17"},{"issue":"1\u20132","key":"17_CR15","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1016\/S0747-7171(89)80022-7","volume":"8","author":"M. Schmidt-Schau\u00df","year":"1989","unstructured":"Schmidt-Schau\u00df, M.: Unification in a combination of arbitrary disjoint equational theories. Journal of Symbolic Computation\u00a08(1\u20132), 51\u2013100 (1989); Special issue on unification. Part II","journal-title":"Journal of Symbolic Computation"},{"issue":"1","key":"17_CR16","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 Computer Science\u00a0290(1), 291\u2013353 (2003)","journal-title":"Theoretical Computer Science"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-19"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-45085-6_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,5]],"date-time":"2019-06-05T22:12:12Z","timestamp":1559772732000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-45085-6_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540405597","9783540450856"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-45085-6_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]}}}