{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T14:58:17Z","timestamp":1725634697525},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540710691"},{"type":"electronic","value":"9783540710707"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-71070-7_30","type":"book-chapter","created":{"date-parts":[[2008,8,29]],"date-time":"2008-08-29T09:56:30Z","timestamp":1220003790000},"page":"332-347","source":"Crossref","is-referenced-by-count":1,"title":["Unification and Matching Modulo Leaf-Permutative Equational Presentations"],"prefix":"10.1007","author":[{"given":"Thierry","family":"Boy de la Tour","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mnacho","family":"Echenim","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Paliath","family":"Narendran","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"30_CR1","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1023\/A:1006439522342","volume":"26","author":"J. Avenhaus","year":"2001","unstructured":"Avenhaus, J., Plaisted, D.: General algorithms for permutations in equational inference. Journal of Automated Reasoning\u00a026, 223\u2013268 (2001)","journal-title":"Journal of Automated Reasoning"},{"key":"30_CR2","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, Cambridge (1998)"},{"key":"30_CR3","doi-asserted-by":"crossref","unstructured":"Bauer, G., Otto, F.: Finite complete rewriting systems and the complexity of the word problem. Acta Informatica\u00a021 (1984)","DOI":"10.1007\/BF00271645"},{"key":"30_CR4","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4613-9771-7","volume-title":"String-rewriting systems","author":"R.V. Book","year":"1993","unstructured":"Book, R.V., Otto, F.: String-rewriting systems. Springer, Heidelberg (1993)"},{"key":"30_CR5","series-title":"Lecture Notes in Computer Science","volume-title":"Term Rewriting and Applications","author":"T. Tour Boy de la","year":"2007","unstructured":"Boy de la Tour, T., Echenim, M.: Determining unify-stable presentations. In: Baader, F. (ed.) RTA 2007. LNCS, vol.\u00a04533, Springer, Heidelberg (2007)"},{"issue":"4","key":"30_CR6","doi-asserted-by":"crossref","first-page":"624","DOI":"10.1016\/j.ic.2006.11.001","volume":"25","author":"T. Tour Boy de la","year":"2007","unstructured":"Boy de la Tour, T., Echenim, M.: Permutative rewriting and unification. Information and Computation\u00a025(4), 624\u2013650 (2007)","journal-title":"Information and Computation"},{"issue":"3","key":"30_CR7","first-page":"257","volume":"3","author":"F. Fages","year":"1987","unstructured":"Fages, F.: Associative-commutative unification. JSC\u00a03(3), 257\u2013275 (1987)","journal-title":"JSC"},{"key":"30_CR8","volume-title":"Computers and intractability: a guide to the theory of NP-completeness","author":"M. Garey","year":"1979","unstructured":"Garey, M., Johnson, D.S.: Computers and intractability: a guide to the theory of  NP-completeness. W.H. Freeman, San Francisco (1979)"},{"key":"30_CR9","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1016\/S0747-7171(89)80012-4","volume":"7","author":"J. Siekmann","year":"1989","unstructured":"Siekmann, J.: Unification theory. Journal of Symbolic Computation\u00a07, 207\u2013274 (1989)","journal-title":"Journal of Symbolic Computation"},{"issue":"2","key":"30_CR10","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/BF00245463","volume":"9","author":"D. Kapur","year":"1992","unstructured":"Kapur, D., Narendran, P.: Complexity of unification problems with associative-commutative operators. Journal of Automated Reasoning\u00a09(2), 261\u2013288 (1992)","journal-title":"Journal of Automated Reasoning"},{"key":"30_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"276","DOI":"10.1007\/3-540-52885-7_94","volume-title":"10th International Conference on Automated Deduction","author":"P. Narendran","year":"1990","unstructured":"Narendran, P., Otto, F.: Some results on equational unification. In: Stickel, M.E. (ed.) CADE 1990. LNCS, vol.\u00a0449, pp. 276\u2013291. Springer, Heidelberg (1990)"},{"issue":"1","key":"30_CR12","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1023\/A:1005764526878","volume":"19","author":"P. Narendran","year":"1997","unstructured":"Narendran, P., Otto, F.: Single versus simultaneous equational unification and equational unification for variable-permuting theories. Journal of Automated Reasoning\u00a019(1), 87\u2013115 (1997)","journal-title":"Journal of Automated Reasoning"},{"issue":"4","key":"30_CR13","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1016\/S0747-7171(89)80037-9","volume":"8","author":"M. Schmidt-Schau\u00df","year":"1989","unstructured":"Schmidt-Schau\u00df, M.: Unification in permutative equational theories is undecidable. Journal of Symbolic Computation\u00a08(4), 415\u2013421 (1989)","journal-title":"Journal of Symbolic Computation"},{"issue":"2","key":"30_CR14","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1145\/322261.322262","volume":"28","author":"M.E. Stickel","year":"1981","unstructured":"Stickel, M.E.: A unification algorithm for associative-commutative functions. Journal of the ACM\u00a028(2), 423\u2013434 (1981)","journal-title":"Journal of the ACM"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-71070-7_30.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,3]],"date-time":"2021-05-03T04:36:32Z","timestamp":1620016592000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-71070-7_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540710691","9783540710707"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-71070-7_30","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}