{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,13]],"date-time":"2026-01-13T06:07:10Z","timestamp":1768284430660,"version":"3.49.0"},"reference-count":31,"publisher":"Elsevier BV","issue":"3","license":[{"start":{"date-parts":[[1987,6,1]],"date-time":"1987-06-01T00:00:00Z","timestamp":549504000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":9543,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Symbolic Computation"],"published-print":{"date-parts":[[1987,6]]},"DOI":"10.1016\/s0747-7171(87)80004-4","type":"journal-article","created":{"date-parts":[[2008,3,29]],"date-time":"2008-03-29T14:14:04Z","timestamp":1206800044000},"page":"257-275","source":"Crossref","is-referenced-by-count":38,"title":["Associative-commutative unification"],"prefix":"10.1016","volume":"3","author":[{"given":"Fran\u00e7ois","family":"Fages","sequence":"first","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/S0747-7171(87)80004-4_bib1","series-title":"Complexity of Matching Problems","author":"Benanav","year":"1985"},{"issue":"3","key":"10.1016\/S0747-7171(87)80004-4_bib2","doi-asserted-by":"crossref","first-page":"233","DOI":"10.2307\/2318447","article-title":"Hilbert's Tenth Problem is Unsolvable","volume":"80","author":"Davis","year":"1973","journal-title":"Amer. Math. Monthly"},{"issue":"1","key":"10.1016\/S0747-7171(87)80004-4_bib3","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1016\/0743-1066(84)90022-0","article-title":"On the Sequential Nature of Unification","volume":"1","author":"Dwork","year":"1984","journal-title":"J. of Logic Programming"},{"key":"10.1016\/S0747-7171(87)80004-4_bib4","article-title":"Abstract Properties of Substitutions and Unifiers","author":"Eder","year":"1985","journal-title":"JSC 1"},{"key":"10.1016\/S0747-7171(87)80004-4_bib5","article-title":"Formes canoniques dans les alg\u00e8bres bool\u00e9ennes, et application A la demonstration automatique en logique de premier ordre","author":"Fages","year":"1983","journal-title":"Th\u00e8se, Universit\u00e9 de Paris VI"},{"key":"10.1016\/S0747-7171(87)80004-4_bib6","first-page":"189","article-title":"Unification and Matching in Equational Theories","volume":"43","author":"Fages","year":"1983","journal-title":"CAAP'83, l Aquila, Italy. Lecture Notes in Computer Science 159, March 1983. Theoretical Computer Science"},{"key":"10.1016\/S0747-7171(87)80004-4_bib7","article-title":"Le syst\u00e8me KB: Manuel de R\u00e9f\u00e9rence","author":"Fages","year":"1985","journal-title":"Report n368, INRIA"},{"key":"10.1016\/S0747-7171(87)80004-4_bib8","series-title":"An Algebraic Approach to Unification under Associativity and Commutativity","author":"Fortenbacher","year":"1985"},{"key":"10.1016\/S0747-7171(87)80004-4_bib9","series-title":"SEKIResearch Report","article-title":"Unification in Abelian Semigroups","author":"Herold","year":"1985"},{"key":"10.1016\/S0747-7171(87)80004-4_bib10","series-title":"Combination of Unification Algorithm","author":"Herold","year":"1986"},{"key":"10.1016\/S0747-7171(87)80004-4_bib11","series-title":"Ph.D. Thesis","article-title":"Topics in Automated Theorem Proving and Program Generation","author":"Hsiang","year":"1982"},{"key":"10.1016\/S0747-7171(87)80004-4_bib12","article-title":"R\u00e9solution d'\u00e9quations dans des langages d'ordre .1,2, ... omega","author":"Huet","year":"1976","journal-title":"Th\u00e8se d'Etat, Universit\u00e9 de Paris VII"},{"issue":"3","key":"10.1016\/S0747-7171(87)80004-4_bib13","doi-asserted-by":"crossref","first-page":"144","DOI":"10.1016\/0020-0190(78)90078-9","article-title":"An Algorithm to Generate the Basis of Solutions to Homogenous Linear Diophantine Equations","volume":"7","author":"Huet","year":"1978","journal-title":"Information Processing Letters"},{"key":"10.1016\/S0747-7171(87)80004-4_bib14","series-title":"ormal Languages: Perspectives and Open Problems","article-title":"Equations and Rewrite Rules: a Survey","author":"Huet","year":"1980"},{"key":"10.1016\/S0747-7171(87)80004-4_bib15","series-title":"Associative-Commutative Pattern Matching","author":"Hullot","year":"1979"},{"key":"10.1016\/S0747-7171(87)80004-4_bib16","article-title":"Compilation de Formes Canoniques dans les Theories Equationnelles","author":"Hullot","year":"1980","journal-title":"Th\u00e8se de 3\u00e8me cycle, U. de Paris Sud"},{"key":"10.1016\/S0747-7171(87)80004-4_bib17","article-title":"M\u00e9thodes et outils de conception syst\u00e9matique d'algorithmes d'unification dans les th\u00e9ories \u00e9quationnelles","author":"Kirchner","year":"1985","journal-title":"Th\u00e8se d'\u00e9tat, U. de Nancy"},{"key":"10.1016\/S0747-7171(87)80004-4_bib18","series-title":"Report 84GEN008, General Electric Comp.","article-title":"Abelian Group Unification Algorithm for Elementary Terms","author":"Lankford","year":"1984"},{"key":"10.1016\/S0747-7171(87)80004-4_bib19","series-title":"Internal Report 3\/76","article-title":"Unification of Bags and Sets","author":"Livesey","year":"1976"},{"key":"10.1016\/S0747-7171(87)80004-4_bib20","series-title":"Unification Problems for Combinations of Associativity, Commutativity, Distributivity and Idempotence Axioms","first-page":"161","author":"Livesey","year":"1979"},{"key":"10.1016\/S0747-7171(87)80004-4_bib21","first-page":"233","article-title":"The Problem of Solvability of Equations in a Free Semigroup","author":"Makanin","year":"1977","journal-title":"Akad. Nauk. SSSR, TOM"},{"issue":"2","key":"10.1016\/S0747-7171(87)80004-4_bib22","first-page":"258","article-title":"An Efficient Unification Algorithm","volume":"4","author":"Martelli","year":"1982","journal-title":"ACM T.O.P.L.A.S."},{"key":"10.1016\/S0747-7171(87)80004-4_bib23","series-title":"Diophantine Representation of Recursively Enumerable Predicates","author":"Matiyasevich","year":"1970"},{"issue":"2","key":"10.1016\/S0747-7171(87)80004-4_bib24","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1145\/322248.322251","article-title":"Complete Sets of Reduction for Equational Theories with Complete Unification Algorithms","volume":"28","author":"Peterson","year":"1981","journal-title":"JACM"},{"key":"10.1016\/S0747-7171(87)80004-4_bib25","first-page":"73","article-title":"Building-in Equational Theories","volume":"7","author":"Plotkin","year":"1972","journal-title":"Machine Intelligence"},{"key":"10.1016\/S0747-7171(87)80004-4_bib26","doi-asserted-by":"crossref","DOI":"10.1145\/1089208.1089210","article-title":"A Short. Survey on the State of the Art in Matching and Unification Problems","volume":"13","author":"Raulefs","year":"1979","journal-title":"Sigsam Bulletin"},{"key":"10.1016\/S0747-7171(87)80004-4_bib27","doi-asserted-by":"crossref","first-page":"32","DOI":"10.1145\/321250.321253","article-title":"A Machine Oriented Logic Based on the Resolution Principle","volume":"12","author":"Robinson","year":"1965","journal-title":"JACM"},{"key":"10.1016\/S0747-7171(87)80004-4_bib28","series-title":"A Complete Unification Algorithm for AssociativeCommutative functions","author":"Stickel","year":"1975"},{"issue":"3","key":"10.1016\/S0747-7171(87)80004-4_bib29","doi-asserted-by":"crossref","first-page":"423","DOI":"10.1145\/322261.322262","article-title":"A Unification Algorithm for Associative-Commutative Functions","volume":"28","author":"Stickel","year":"1981","journal-title":"JACM"},{"key":"10.1016\/S0747-7171(87)80004-4_bib30","series-title":"Unification in Combinations of Theories with Collapse-free Axioms and Disjoint Sets of Function Symbols","author":"Tid\u00e9n","year":"1986"},{"key":"10.1016\/S0747-7171(87)80004-4_bib31","series-title":"Combining Unification Algorithms for Confined Equational Theories","author":"Yelick","year":"1985"}],"container-title":["Journal of Symbolic Computation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0747717187800044?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0747717187800044?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2018,12,30]],"date-time":"2018-12-30T17:54:09Z","timestamp":1546192449000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0747717187800044"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1987,6]]},"references-count":31,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1987,6]]}},"alternative-id":["S0747717187800044"],"URL":"https:\/\/doi.org\/10.1016\/s0747-7171(87)80004-4","relation":{},"ISSN":["0747-7171"],"issn-type":[{"value":"0747-7171","type":"print"}],"subject":[],"published":{"date-parts":[[1987,6]]}}}