{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T17:09:21Z","timestamp":1725728961979},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642385735"},{"type":"electronic","value":"9783642385742"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-38574-2_17","type":"book-chapter","created":{"date-parts":[[2013,6,4]],"date-time":"2013-06-04T07:55:13Z","timestamp":1370332513000},"page":"249-266","source":"Crossref","is-referenced-by-count":6,"title":["Hierarchical Combination"],"prefix":"10.1007","author":[{"given":"Serdar","family":"Erbatur","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Deepak","family":"Kapur","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrew M.","family":"Marshall","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Paliath","family":"Narendran","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christophe","family":"Ringeissen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"17_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/978-3-642-28332-1_7","volume-title":"Language and Automata Theory and Applications","author":"S. Anantharaman","year":"2012","unstructured":"Anantharaman, S., Bouchard, C., Narendran, P., Rusinowitch, M.: Unification modulo chaining. In: Dediu, A.-H., Mart\u00edn-Vide, C. (eds.) LATA 2012. LNCS, vol.\u00a07183, pp. 70\u201382. Springer, Heidelberg (2012)"},{"key":"17_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1007\/978-3-642-31365-3_4","volume-title":"Automated Reasoning","author":"S. Anantharaman","year":"2012","unstructured":"Anantharaman, S., Erbatur, S., Lynch, C., Narendran, P., Rusinowitch, M.: Unification modulo synchronous distributivity. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol.\u00a07364, pp. 14\u201329. Springer, Heidelberg (2012)"},{"key":"17_CR3","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/978-3-540-25984-8_11","volume-title":"Automated Reasoning","author":"F. Baader","year":"2004","unstructured":"Baader, F., Ghilardi, S., Tinelli, C.: A new combination procedure for the word problem that generalizes fusion decidability results in modal logics. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol.\u00a03097, pp. 183\u2013197. Springer, Heidelberg (2004)"},{"key":"17_CR4","doi-asserted-by":"crossref","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, New York (1998)"},{"issue":"2","key":"17_CR5","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_CR6","doi-asserted-by":"crossref","unstructured":"Baader, F., Snyder, W.: Unification theory. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 445\u2013532. Elsevier and MIT Press (2001)","DOI":"10.1016\/B978-044450813-3\/50010-2"},{"key":"17_CR7","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/10720084_17","volume-title":"Proceedings of the 3rd International Workshop on Frontiers of Combining Systems, (FroCoS 2000)","author":"F. Baader","year":"2000","unstructured":"Baader, F., Tinelli, C.: Combining equational theories sharing non-collapse-free constructors. In: Kirchner, H. (ed.) FroCos 2000. LNCS (LNAI), vol.\u00a01794, pp. 260\u2013274. Springer, Heidelberg (2000)"},{"key":"17_CR8","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_CR9","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"},{"issue":"1-2","key":"17_CR10","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/S0747-7171(89)80021-5","volume":"8","author":"H.-J. B\u00fcrckert","year":"1989","unstructured":"B\u00fcrckert, H.-J., Herold, A., Schmidt-Schau\u00df, M.: On equational theories, unification, and (un)decidability. Journal of Symbolic Computation\u00a08(1-2), 3\u201349 (1989)","journal-title":"Journal of Symbolic Computation"},{"key":"17_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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 non-disjoint equational theories. In: Bundy, A. (ed.) CADE 1994. LNCS, vol.\u00a0814, pp. 267\u2013281. Springer, Heidelberg (1994)"},{"issue":"4","key":"17_CR12","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1016\/0747-7171(92)90010-2","volume":"14","author":"D.J. Dougherty","year":"1992","unstructured":"Dougherty, D.J., Johann, P.: An improved general E-unification method. Journal of Symbolic Computation\u00a014(4), 303\u2013320 (1992)","journal-title":"Journal of Symbolic Computation"},{"issue":"2-4","key":"17_CR13","first-page":"109","volume":"16","author":"S. Erbatur","year":"2011","unstructured":"Erbatur, S., Marshall, A.M., Kapur, D., Narendran, P.: Unification over distributive exponentiation (sub)theories. Journal of Automata, Languages and Combinatorics (JALC)\u00a016(2-4), 109\u2013140 (2011)","journal-title":"Journal of Automata, Languages and Combinatorics (JALC)"},{"issue":"2-3","key":"17_CR14","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1016\/0304-3975(89)90004-2","volume":"67","author":"J.H. Gallier","year":"1989","unstructured":"Gallier, J.H., Snyder, W.: Complete sets of transformations for general E-unification. Theoretical Computer Science\u00a067(2-3), 203\u2013260 (1989)","journal-title":"Theoretical Computer Science"},{"issue":"4","key":"17_CR15","doi-asserted-by":"publisher","first-page":"797","DOI":"10.1145\/322217.322230","volume":"27","author":"G.P. Huet","year":"1980","unstructured":"Huet, G.P.: Confluent reductions: Abstract properties and applications to term rewriting systems. Journal of the ACM (JACM)\u00a027(4), 797\u2013821 (1980)","journal-title":"Journal of the ACM (JACM)"},{"key":"17_CR16","doi-asserted-by":"crossref","unstructured":"Jouannaud, J.-P., Kirchner, C.: Solving equations in abstract algebras: A rule-based survey of unification. In: Computational Logic - Essays in Honor of Alan Robinson, pp. 257\u2013321 (1991)","DOI":"10.1016\/0743-1066(92)90027-Z"},{"key":"17_CR17","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/s10817-007-9068-z","volume":"39","author":"B. Morawska","year":"2007","unstructured":"Morawska, B.: General E-unification with eager variable elimination and a nice cycle rule. Journal of Automated Reasoning\u00a039, 77\u2013106 (2007)","journal-title":"Journal of Automated Reasoning"},{"key":"17_CR18","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)"},{"key":"17_CR19","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, 51\u201399 (1989)","journal-title":"Journal of Symbolic Computation"},{"key":"17_CR20","doi-asserted-by":"crossref","unstructured":"Snyder, W.: A Proof Theory for General Unification, Birkhauser. Progress in Computer Science and Applied Logic, vol.\u00a011 (1991)","DOI":"10.1007\/978-1-4612-0435-0_4"},{"key":"17_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"431","DOI":"10.1007\/3-540-16780-3_110","volume-title":"8th International Conference on Automated Deduction","author":"E. Tid\u00e9n","year":"1986","unstructured":"Tid\u00e9n, E.: Unification in combinations of collapse-free theories with disjoint sets of function symbols. In: Siekmann, J.H. (ed.) CADE 1986. LNCS, vol.\u00a0230, pp. 431\u2013449. Springer, Heidelberg (1986)"},{"issue":"1-2","key":"17_CR22","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1016\/S0747-7171(87)80025-1","volume":"3","author":"K.A. Yelick","year":"1987","unstructured":"Yelick, K.A.: Unification in combinations of collapse-free regular theories. Journal of Symbolic Computation\u00a03(1-2), 153\u2013181 (1987)","journal-title":"Journal of Symbolic Computation"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-24"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-38574-2_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,13]],"date-time":"2019-05-13T17:57:55Z","timestamp":1557770275000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-38574-2_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642385735","9783642385742"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-38574-2_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}