{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,31]],"date-time":"2025-05-31T04:10:31Z","timestamp":1748664631036,"version":"3.41.0"},"publisher-location":"Cham","reference-count":19,"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":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-24246-0_18","type":"book-chapter","created":{"date-parts":[[2015,9,19]],"date-time":"2015-09-19T04:20:53Z","timestamp":1442636453000},"page":"291-306","source":"Crossref","is-referenced-by-count":4,"title":["Unification and Matching in Hierarchical Combinations of Syntactic Theories"],"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","published-online":{"date-parts":[[2015,11,12]]},"reference":[{"key":"18_CR1","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, New York (1998)"},{"issue":"2","key":"18_CR2","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":"18_CR3","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"},{"issue":"6","key":"18_CR4","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":"18_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"446","DOI":"10.1007\/BFb0013843","volume-title":"Algebraic and Logic Programming","author":"A. Boudet","year":"1992","unstructured":"Boudet, A., Contejean, E.: On n-syntactic equational theories. In: Kirchner, H., Levi, G. (eds.) ALP 1992. LNCS, vol.\u00a0632, pp. 446\u2013457. Springer, Heidelberg (1992)"},{"issue":"1","key":"18_CR6","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1006\/inco.1994.1043","volume":"111","author":"H. Comon","year":"1994","unstructured":"Comon, H., Haberstrau, M., Jouannaud, J.: Syntacticness, cycle-syntacticness, and shallow theories. Inf. Comput.\u00a0111(1), 154\u2013191 (1994)","journal-title":"Inf. Comput."},{"key":"18_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/978-3-642-38574-2_17","volume-title":"Automated Deduction \u2013 CADE-24","author":"S. Erbatur","year":"2013","unstructured":"Erbatur, S., Kapur, D., Marshall, A.M., Narendran, P., Ringeissen, C.: Hierarchical combination. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol.\u00a07898, pp. 249\u2013266. Springer, Heidelberg (2013)"},{"key":"18_CR8","unstructured":"Erbatur, S., Kapur, D., Marshall, A.M., Narendran, P., Ringeissen, C.: Hierarchical combination of matching algorithms. In: Twentyeighth International Workshop on Unification (UNIF 2014), Vienna, Austria (2014)"},{"issue":"2\u20134","key":"18_CR9","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\u20134), 109\u2013140 (2011)","journal-title":"Journal of Automata, Languages and Combinatorics (JALC)"},{"issue":"2\u20133","key":"18_CR10","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\u20133), 203\u2013260 (1989)","journal-title":"Theoretical Computer Science"},{"key":"18_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/BFb0029593","volume-title":"Mathematical Foundations of Computer Science 1990","author":"J.-P. Jouannaud","year":"1990","unstructured":"Jouannaud, J.-P.: Syntactic theories. In: Rovan, B. (ed.) MFCS 1990. LNCS, vol.\u00a0452, pp. 15\u201325. Springer, Heidelberg (1990)"},{"key":"18_CR12","doi-asserted-by":"crossref","unstructured":"Kirchner, C., Klay, F.: Syntactic theories and unification. In: Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science Logic in Computer Science, LICS 1990, pp. 270\u2013277, June1990","DOI":"10.1109\/LICS.1990.113753"},{"key":"18_CR13","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"471","DOI":"10.1007\/3-540-45620-1_37","volume-title":"Automated Deduction - CADE-18","author":"C. Lynch","year":"2002","unstructured":"Lynch, C., Morawska, B.: Basic syntactic mutation. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol.\u00a02392, pp. 471\u2013485. Springer, Heidelberg (2002)"},{"issue":"1","key":"18_CR14","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1998.2730","volume":"147","author":"R. Nieuwenhuis","year":"1998","unstructured":"Nieuwenhuis, R.: Decidability and complexity analysis by basic paramodulation. Inf. Comput.\u00a0147(1), 1\u201321 (1998)","journal-title":"Inf. Comput."},{"key":"18_CR15","doi-asserted-by":"crossref","unstructured":"Nipkow, T.: Proof transformations for equational theories. In: Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science Logic in Computer Science, LICS 1990, pp. 278\u2013288, June 1990","DOI":"10.1109\/LICS.1990.113754"},{"issue":"6","key":"18_CR16","doi-asserted-by":"publisher","first-page":"633","DOI":"10.1016\/S0747-7171(08)80145-9","volume":"12","author":"T. Nipkow","year":"1991","unstructured":"Nipkow, T.: Combining matching algorithms: The regular case. J. Symb. Comput.\u00a012(6), 633\u2013654 (1991)","journal-title":"J. Symb. Comput."},{"issue":"2","key":"18_CR17","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. Inf. Comput.\u00a0126(2), 144\u2013160 (1996)","journal-title":"Inf. Comput."},{"key":"18_CR18","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":"18_CR19","doi-asserted-by":"crossref","unstructured":"Snyder, W.: A Proof Theory for General Unification. Progress in Computer Science and Applied Logic, vol.\u00a011. Birkh\u00e4user (1991)","DOI":"10.1007\/978-1-4612-0435-0"}],"container-title":["Lecture Notes in Computer Science","Frontiers of Combining Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-24246-0_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,30]],"date-time":"2025-05-30T18:26:25Z","timestamp":1748629585000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-24246-0_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319242453","9783319242460"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-24246-0_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}