{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T22:58:36Z","timestamp":1725663516344},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540563938"},{"type":"electronic","value":"9783540475491"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1993]]},"DOI":"10.1007\/3-540-56393-8_38","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T11:08:20Z","timestamp":1330254500000},"page":"468-482","source":"Crossref","is-referenced-by-count":0,"title":["A new approach to general E-unification based on conditional rewriting systems"],"prefix":"10.1007","author":[{"given":"Bertrand","family":"Delsart","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,5,30]]},"reference":[{"key":"38_CR1","doi-asserted-by":"crossref","unstructured":"F. Baader and K.U. Schulz. Unification in the union of disjoint equational theories: Combining decision procedures. In Proceedings of the 11th Conference on Automated Deduction, pages 50\u201365. Springer-Verlag, LNAI 607, 1992.","DOI":"10.1007\/3-540-55602-8_155"},{"key":"38_CR2","doi-asserted-by":"crossref","unstructured":"T. Boy de la Tour, R. Caferra, and G. Chaminade. Some tools for an inference laboratory (ATINF). In Proceedings of the 9th Conference on Automated Deduction, pages 744\u2013745. Springer-Verlag, LNCS 310, 1988.","DOI":"10.1007\/BFb0012877"},{"key":"38_CR3","doi-asserted-by":"crossref","unstructured":"H. Chen, J. Hsiang, and H.-C. Kong. On finite representation of infinite sequences of terms. In Proceedings of the 2nd international Conditional and Typed Rewriting Systems workshop, pages 100\u2013114. Springer-Verlag, LNCS 516, 1990.","DOI":"10.1007\/3-540-54317-1_83"},{"key":"38_CR4","unstructured":"H. Comon, K. Haberstrau, and J.-P. Jouannaud. Decidable problems in shallow equational theories. In Proceeding of the 7th IEEE Symposium on Logic in Computer Science, 1991."},{"key":"38_CR5","unstructured":"J. Corbin and M. Bidoit. A rehabilitation of Robinson's unification algorithm. In R. Mason, editor, Proceedings of the IFIP'83, pages 909\u2013914, 1983."},{"key":"38_CR6","doi-asserted-by":"crossref","unstructured":"M. Davis. The prehistory and early history of automated deduction. In J. Siekmann and G. Wrighston, editors, Automation of Reasoning 1, Classical Papers on Computational Logic 1957\u20131966. Springer-Verlag, 1983.","DOI":"10.1007\/978-3-642-81952-0_1"},{"key":"38_CR7","unstructured":"B. Delsart. General E-unification: A realistic approach. Presented at UNIF'91, 1991. (extended abstract)."},{"key":"38_CR8","unstructured":"B. Delsart. Efficient E-unification algorithms. Technical report, INPG, 1992."},{"key":"38_CR9","doi-asserted-by":"crossref","unstructured":"N. Dershowitz and J.-P. Jouannaud. Hanbook on Theoretical Computer Science, volume B, chapter 6: Rewrite Systems, pages 243\u2013320. J. van Leeuwen (ed.), 1990.","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"key":"38_CR10","first-page":"162","volume":"43","author":"N. Dershowitz","year":"1991","unstructured":"N. Dershowitz and J.-P. Jouannaud. Notations for rewriting. EATCS, 43:162\u2013172, 1991.","journal-title":"EATCS"},{"key":"38_CR11","doi-asserted-by":"crossref","unstructured":"D. Dougherty and P. Johann. An improved general E-unification method. In Proceedings of the 10th Conference on Automated Deduction, pages 261\u2013275. Springer-Verlag, LNCS 449, 1990.","DOI":"10.1007\/3-540-52885-7_93"},{"key":"38_CR12","unstructured":"M. Fay. First order unification in equational theories. In Proceedings of the 4th Workshop on Automated Deduction, pages 162\u2013167, 1979."},{"key":"38_CR13","doi-asserted-by":"crossref","unstructured":"J.H. Gallier and W. Snyder. A general complete E-unification procedure. In Proceeding of the 2nd Conference on Rewrite Techniques and Applications, pages 216\u2013227. Springer-Verlag, LNCS 256, 1987.","DOI":"10.1007\/3-540-17220-3_19"},{"issue":"23","key":"38_CR14","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1016\/0304-3975(89)90004-2","volume":"67","author":"J. H. Gallier","year":"1989","unstructured":"J.H. Gallier and W. Snyder. Complete sets of transformations for general E-unification. Theoretical Computer Science, 67(2,3):203\u2013260, 1989.","journal-title":"Theoretical Computer Science"},{"key":"38_CR15","unstructured":"J. Herbrand. Recherche sur la th\u00e9orie de la d\u00e9monstration, 1930. Th\u00e8se de doctorat, Universit\u00e9 de Paris."},{"key":"38_CR16","doi-asserted-by":"crossref","unstructured":"A. Herold. Combination of unification algorithms. In Proceedings of the 8th Conference on Automated Deduction, pages 450\u2013469. Springer-Verlag, LNCS 230, 1986.","DOI":"10.1007\/3-540-16780-3_111"},{"key":"38_CR17","unstructured":"G. Huet. R\u00e9solution d'\u00e9quations dans les langages d'ordre 1,2,...,\u221e. Th\u00e8se d'Etat, Universit\u00e9 de Paris, 1976."},{"key":"38_CR18","doi-asserted-by":"crossref","unstructured":"J.-M. Hullot. Canonical forms and unification. In Proceedings of the 5th Conference on Automated Deduction, pages 318\u2013334. Springer-Verlag, LNCS 87, 1980.","DOI":"10.21236\/ADA087640"},{"key":"38_CR19","unstructured":"J.-P. Jouannaud and C. Kirchner. Solving equations in abstract algebras: A rule-based survey of unification. Technical Report 561, LRI, 1990."},{"key":"38_CR20","unstructured":"C. Kirchner. Computing unification algorithms. In Proceedings of the first IEEE Symposium on Logic in Computer Science, pages 206\u2013216, 1986."},{"key":"38_CR21","doi-asserted-by":"crossref","first-page":"303","DOI":"10.1016\/0304-3975(89)90007-8","volume":"67","author":"H. Kirchner","year":"1989","unstructured":"H. Kirchner. Schematization of infinite sets of rewrite rules generated by divergent completion processes. Theoretical Computer Science, 67:303\u2013332, 1989.","journal-title":"Theoretical Computer Science"},{"key":"38_CR22","doi-asserted-by":"crossref","unstructured":"H. Kirchner and M. Hermann. Meta-rule synthesis for crossed rewrite systems. In Proceedings of the 2nd international Conditional and Typed Rewriting Systems workshop, pages 143\u2013154. Springer-Verlag, LNCS 516, 1990.","DOI":"10.1007\/3-540-54317-1_87"},{"issue":"2","key":"38_CR23","doi-asserted-by":"crossref","first-page":"258","DOI":"10.1145\/357162.357169","volume":"4","author":"A. Martelli","year":"1982","unstructured":"A. Martelli and U. Montanari. An efficient unification algorithm. ACM Transaction on Programming Languages And Systems, 4(2):258\u2013282, 1982.","journal-title":"ACM Transaction on Programming Languages And Systems"},{"issue":"3","key":"38_CR24","doi-asserted-by":"crossref","first-page":"295","DOI":"10.1016\/S0747-7171(89)80014-8","volume":"7","author":"W. Nutt","year":"1989","unstructured":"W. Nutt, P. Rety, and G. Smolka. Basic narrowing revisited. Journal of Symbolic Computation, 7(3,4):295\u2013318, 1989.","journal-title":"Journal of Symbolic Computation"},{"key":"38_CR25","doi-asserted-by":"crossref","first-page":"158","DOI":"10.1016\/0022-0000(78)90043-0","volume":"16","author":"M. S. Paterson","year":"1978","unstructured":"M.S. Paterson and M.N. Wegman. Linear unification. Journal of Computer Systems, Sciences, 16:158\u2013167, 1978.","journal-title":"Journal of Computer Systems, Sciences"},{"key":"38_CR26","doi-asserted-by":"crossref","unstructured":"P. Rety. Improving basic narrowing. In Proceedings of the 2nd Conference on Rewriting Techniques and Applications, pages 226\u2013241. Springer-Verlag, LNCS 256, 1987.","DOI":"10.1007\/3-540-17220-3_20"},{"issue":"1","key":"38_CR27","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"A. Robinson","year":"1965","unstructured":"A. Robinson. A machine-oriented logic based on the resolution principle. Journal of the Association for Computing Machinery, 12(1):23\u201341, 1965.","journal-title":"Journal of the Association for Computing Machinery"},{"key":"38_CR28","unstructured":"M. Schmidt-Schau\u00df. Unification in a combination of arbitrary disjoint equational theories. Seki report sr-87-16, University of Kaiserslauterm, 1987."}],"container-title":["Lecture Notes in Computer Science","Conditional Term Rewriting Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-56393-8_38.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:03:38Z","timestamp":1605647018000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-56393-8_38"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993]]},"ISBN":["9783540563938","9783540475491"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/3-540-56393-8_38","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1993]]}}}