{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T21:40:23Z","timestamp":1742593223140,"version":"3.40.2"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540539049"},{"type":"electronic","value":"9783540463832"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1991]]},"DOI":"10.1007\/3-540-53904-2_89","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T22:16:34Z","timestamp":1330208194000},"page":"98-111","source":"Crossref","is-referenced-by-count":0,"title":["AC unification through order-sorted AC1 unification"],"prefix":"10.1007","author":[{"given":"Eric","family":"Domenjoud","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,7]]},"reference":[{"key":"9_CR1","doi-asserted-by":"crossref","unstructured":"T.B. Baird, G.E. Peterson, and R.W. Wilkerson. Complete sets of reductions modulo associativity, commutativity and identity. In N. Dershowitz, editor, Proceedings of RTA '89, Chapel Hill, (North Carolina, USA), volume 355 of LNCS, pages 29\u201344. Springer-Verlag, 1989.","DOI":"10.1007\/3-540-51081-8_98"},{"key":"9_CR2","unstructured":"A. Boudet. Unification dans les m\u00e9langes de th\u00e9ories \u00e9quationelles. application aux axiomes d'associativit\u00e9, commutativit\u00e9, identit\u00e9 et idempotence, aux anneaux bool\u00e9ens, et aux groupes ab\u00e9liens. Th\u00e8se de l'Universit\u00e9 d'Orsay, 1990."},{"key":"9_CR3","unstructured":"W. Buntine and H.-J. B\u00fcrckert. On solving equations and disequations. Technical Report SR-89-03, Universit\u00e4t Kaiserslautern, 1989."},{"key":"9_CR4","first-page":"201","volume":"8","author":"M. Clausen","year":"1989","unstructured":"M. Clausen and A. Fortenbacher. Efficient solution of linear diophantine equations. JSC, 8:201\u2013216, 1989. Special issue on unification.","journal-title":"JSC"},{"key":"9_CR5","unstructured":"E. Contejean and H. Devie. Solving systems of linear diophantine equations. In H.-J. B\u00fcrckert and W. Nutt, editors, Proceedings of UNIF'89, Lambrecht (Germany), 1989."},{"key":"9_CR6","series-title":"Research Report","volume-title":"AC-unification through order-sorted AC1-unification","author":"E. Domenjoud","year":"1989","unstructured":"E. Domenjoud. AC-unification through order-sorted AC1-unification. Research Report 89-R-67, CRIN, Nancy (France), 1989."},{"key":"9_CR7","series-title":"Research Report","volume-title":"Number of minimal unifiers of the equation $$\\alpha x_1 + \\cdots + \\alpha x_p \\dot = _{AC} \\beta y_1 + \\cdots + \\beta y_q$$","author":"E. Domenjoud","year":"1989","unstructured":"E. Domenjoud. Number of minimal unifiers of the equation $$\\alpha x_1 + \\cdots + \\alpha x_p \\dot = _{AC} \\beta y_1 + \\cdots + \\beta y_q$$ . Research Report 89-R-2, CRIN, Nancy (France), 1989. To appear in JAR (1990)."},{"key":"9_CR8","doi-asserted-by":"crossref","unstructured":"E. Domenjoud. Solving systems of linear diophantine equations: an algebraic approach. In Proceedings of UNIF'90, Leeds (U.K.), 1990.","DOI":"10.1007\/3-540-54345-7_57"},{"key":"9_CR9","doi-asserted-by":"crossref","unstructured":"F. Fages. Associative-commutative unification. In R. Shostak, editor, Proceedings of CADE'84, Napa Valley (California, USA), volume 170 of LNCS, pages 194\u2013208. Springer-Verlag, 1984.","DOI":"10.1007\/978-0-387-34768-4_12"},{"key":"9_CR10","doi-asserted-by":"crossref","first-page":"247","DOI":"10.1007\/BF00243791","volume":"3","author":"A. Herold","year":"1987","unstructured":"A. Herold and J. Siekmann. Unification in abelian semigroups. JAR, 3:247\u2013283, 1987.","journal-title":"JAR"},{"key":"9_CR11","doi-asserted-by":"crossref","first-page":"144","DOI":"10.1016\/0020-0190(78)90078-9","volume":"7","author":"G. Huet","year":"1978","unstructured":"G. Huet. An algorithm to generate the basis of solutions to homogenous linear diophantine equations. Information Processing Letters, 7:144\u2013147, 1978.","journal-title":"Information Processing Letters"},{"key":"9_CR12","unstructured":"J.-M. Hullot. Associative-commutative pattern matching. In Proceedings 9th International Joint Conference on Artificial Intelligence, 1979."},{"key":"9_CR13","unstructured":"C. Kirchner. M\u00e9thodes et outils de conception syst\u00e9matique d'algorithmes d'unification dans les th\u00e9ories \u00e9quationnelles. Th\u00e8se d'\u00e9tat, Universit\u00e9 de Nancy I, 1985."},{"key":"9_CR14","unstructured":"C. Kirchner. From unification in combination of equational to a new AC-unification algorithm. Technical Report 87-R-132, Centre de Recherche en Informatique de Nancy, 1987."},{"key":"9_CR15","unstructured":"C. Kirchner. Order-sorted equational unification. Presented at the fifth International Conference on Logic Programming (Seattle, USA), 1988. Also as rapport de recherche INRIA 954."},{"key":"9_CR16","doi-asserted-by":"crossref","unstructured":"C. Kirchner and H. Kirchner. Constrained equational reasoning. In Proceedings of the ACM-SIGSAM 1989 International Symposium on Symbolic and Algebraic Computation, pages 382\u2013389, Portland (Oregon), 1989. ACM Press. Report CRIN 89-R-220.","DOI":"10.1145\/74540.74585"},{"key":"9_CR17","first-page":"39","volume":"305","author":"J.-L. Lambert","year":"1987","unstructured":"J.-L. Lambert. Une borne pour les g\u00e9n\u00e9rateurs des solutions enti\u00e8res positives d'une \u00e9quation diophantienne lin\u00e9aire. Compte-rendu de L'Acad\u00e9mie des Sciences de Paris, 305:39\u201340, 1987.","journal-title":"Compte-rendu de L'Acad\u00e9mie des Sciences de Paris"},{"key":"9_CR18","first-page":"217","volume":"8","author":"P. Lincoln","year":"1989","unstructured":"P. Lincoln and J. Christian. Adventures in associative-commutative unification. JSC, 8:217\u2013240, 1989. Special issue on unification.","journal-title":"JSC"},{"key":"9_CR19","unstructured":"M. Livesey and J. Siekmann. Unification of bags and sets. Technical report, Institut f\u00fcr Informatik I, Universit\u00e4t Karlsruhe, 1976."},{"key":"9_CR20","first-page":"51","volume":"8","author":"M. Schmidt-Schau\u00df","year":"1989","unstructured":"M. Schmidt-Schau\u00df. Combination of unification algorithms. JSC, 8:51\u2013100, 1989. Special issue on unification.","journal-title":"JSC"},{"key":"9_CR21","doi-asserted-by":"crossref","unstructured":"G. Smolka, W. Nutt, J.A. Goguen, and J. Meseguer. Order-sorted equational computation. In H. Ait-Kaci and M. Nivat, editors, Resolution of Equations in Algebraic Structures, Volume 2: Rewriting Techniques, pages 297\u2013367. Academic Press, 1989.","DOI":"10.1016\/B978-0-12-046371-8.50016-X"},{"key":"9_CR22","doi-asserted-by":"crossref","unstructured":"M.E. Stickel. A complete unification algorithm for associative-commutative functions. Proceedings 4th International Joint Conference on Artificial Intelligence, Tbilissi, 1975.","DOI":"10.21236\/ADA015846"}],"container-title":["Lecture Notes in Computer Science","Rewriting Techniques and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-53904-2_89.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T21:11:52Z","timestamp":1742591512000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-53904-2_89"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1991]]},"ISBN":["9783540539049","9783540463832"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/3-540-53904-2_89","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1991]]}}}