{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,30]],"date-time":"2022-03-30T13:26:04Z","timestamp":1648646764010},"reference-count":40,"publisher":"Elsevier BV","issue":"1","license":[{"start":{"date-parts":[[1992,7,1]],"date-time":"1992-07-01T00:00:00Z","timestamp":709948800000},"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":7686,"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":[[1992,7]]},"DOI":"10.1016\/0747-7171(92)90025-y","type":"journal-article","created":{"date-parts":[[2004,12,9]],"date-time":"2004-12-09T22:58:50Z","timestamp":1102633130000},"page":"51-70","source":"Crossref","is-referenced-by-count":5,"title":["AC-unification race: The system solving approach, implementation and benchmarks"],"prefix":"10.1016","volume":"14","author":[{"given":"Mohamed","family":"Adi","sequence":"first","affiliation":[]},{"given":"Claude","family":"Kirchner","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/0747-7171(92)90025-Y_BIB1","article-title":"Etude et implantation d'algorithmes d'unification associative commutative","author":"Adi","year":"1988"},{"key":"10.1016\/0747-7171(92)90025-Y_BIB2","article-title":"Calculs associatif et commutatifs. Etude et r\u00e9alisation du syst\u00e8me UNIFAC","author":"Adi","year":"1991"},{"key":"10.1016\/0747-7171(92)90025-Y_BIB3","author":"Bert","year":"1989"},{"key":"10.1016\/0747-7171(92)90025-Y_BIB4","article-title":"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","author":"Boudet","year":"1990"},{"key":"10.1016\/0747-7171(92)90025-Y_BIB5","series-title":"Proceedings 10th International Conference on Automated Deduction","article-title":"Unification in a combination of equational theories: An efficient algorithm","volume":"volume 449","author":"Boudet","year":"1990"},{"key":"10.1016\/0747-7171(92)90025-Y_BIB6","series-title":"Competing for the AC-unification race","author":"Boudet","year":"1991"},{"key":"10.1016\/0747-7171(92)90025-Y_BIB7","series-title":"Proceedings 5th IEEE Symposium on Logic in Computer Science","first-page":"289","article-title":"A new AC unification algorithm with a new algorithm for solving diophantine equations","author":"Boudet","year":"1990"},{"issue":"1","key":"10.1016\/0747-7171(92)90025-Y_BIB8","doi-asserted-by":"crossref","first-page":"465","DOI":"10.1007\/BF00297251","article-title":"Opening the AC-unification race","volume":"4","author":"B\u00fcrckert","year":"1988","journal-title":"Journal of Automated Reasoning"},{"issue":"1 & 2","key":"10.1016\/0747-7171(92)90025-Y_BIB9","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/S0747-7171(89)80021-5","article-title":"On equational theories, unification and decidability","volume":"8","author":"B\u00fcrckert","year":"1989","journal-title":"Journal of Symbolic Computation"},{"key":"10.1016\/0747-7171(92)90025-Y_BIB10","series-title":"Unification","first-page":"377","article-title":"Efficient solution of linear diophantine equations","author":"Clausen","year":"1990"},{"key":"10.1016\/0747-7171(92)90025-Y_BIB11","article-title":"R\u00e9solution de syst\u00e8mes lin\u00e9aires d'\u00e9quations diophantiennes","author":"Contejean","year":"1991","journal-title":"Compterendus de l'Acad\u00e9mie des Sciences de Paris"},{"key":"10.1016\/0747-7171(92)90025-Y_BIB12","article-title":"Number of minimal unifiers of the equations \u03b1x1 +\u22ef+\u03b1xp \u2250 AC \u03b2y1 + \u22ef + \u03b2yq","author":"Domenjoud","year":"1989"},{"key":"10.1016\/0747-7171(92)90025-Y_BIB13","series-title":"Proceedings 16th International Symposium on Mathematical Foundations of Computer Science","first-page":"141","article-title":"Solving systems of linear diophantine equations: An algebraic approach","volume":"volume 520","author":"Domenjoud","year":"1991"},{"key":"10.1016\/0747-7171(92)90025-Y_BIB14","series-title":"Proceedings 7th International Conference on Automated Deduction","first-page":"194","article-title":"Associative-commutative unification","volume":"volume 170","author":"Fages","year":"1984"},{"key":"10.1016\/0747-7171(92)90025-Y_BIB15","article-title":"Algebraische unifikation","author":"Fortenbacher","year":"1983"},{"key":"10.1016\/0747-7171(92)90025-Y_BIB16","series-title":"Logic Programming. Functions, relations and equations","article-title":"EQLOG: Equality, types and generic modules for logic programming","author":"Goguen","year":"1986"},{"key":"10.1016\/0747-7171(92)90025-Y_BIB17","doi-asserted-by":"crossref","first-page":"247","DOI":"10.1007\/BF00243791","article-title":"Unification in abelian semigroups","volume":"3","author":"Herold","year":"1987","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/0747-7171(92)90025-Y_BIB18","article-title":"Combination of Unification Algorithms in Equational Theories","author":"Herold","year":"1987"},{"issue":"3","key":"10.1016\/0747-7171(92)90025-Y_BIB19","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\/0747-7171(92)90025-Y_BIB20","article-title":"Compilation de Formes Canoniques dans les Th\u00e9ories \u00e9quationelles","author":"Hullot","year":"1980"},{"key":"10.1016\/0747-7171(92)90025-Y_BIB21","series-title":"Computational Logic. Essays in honor of Alan Robinson","first-page":"257","article-title":"Solving equations in abstract algebras: a rule-based survey of unification","author":"Jouannaud","year":"1991"},{"key":"10.1016\/0747-7171(92)90025-Y_BIB22","series-title":"Proceedings 8th International Conference on Automated Deduction","article-title":"NP-completeness of the set unification and matching problems","volume":"volume 230","author":"Kapur","year":"1986"},{"key":"10.1016\/0747-7171(92)90025-Y_BIB23","series-title":"Proceedings of LICS'92","article-title":"Double-exponential complexity of computing a complete set of AC-unifiers","author":"Kapur","year":"1992"},{"key":"10.1016\/0747-7171(92)90025-Y_BIB24","article-title":"An improved upper bound for nonnegative basis solutions of a linear diophantine equation","author":"Kapur","year":"1989"},{"key":"10.1016\/0747-7171(92)90025-Y_BIB25","article-title":"M\u00e9thodes et outils de conception syst\u00e9matique d'algorithmes d'unification dans les th\u00e9ories \u00e9quationnelles","author":"Kirchner","year":"1985"},{"key":"10.1016\/0747-7171(92)90025-Y_BIB26","series-title":"Resolution of Equations in Algebraic Structures, Volume 2: Rewriting Techniques","first-page":"171","article-title":"From unification in combination theories to a new AC-unification algorithm","author":"Kirchner","year":"1989"},{"issue":"3","key":"10.1016\/0747-7171(92)90025-Y_BIB27","first-page":"9","article-title":"Deduction with symbolic constraints","volume":"4","author":"Kirchner","year":"1990","journal-title":"Revue d'Intelligence Artificielle"},{"issue":"1","key":"10.1016\/0747-7171(92)90025-Y_BIB28","first-page":"39","article-title":"Une borne pour les g\u00e9n\u00e9rateurs des solutions enti\u00e8res positives d'une \u00e9quation diophantienne lin\u00e9aire","volume":"305","author":"Lambert","year":"1987","journal-title":"Compte-rendus de l'Acad\u00e9mie des Sciences de Paris"},{"key":"10.1016\/0747-7171(92)90025-Y_BIB29","doi-asserted-by":"crossref","DOI":"10.1007\/BF00245019","article-title":"Non-negative integer basis algorithms for linear equations with integer coefficients","author":"Lankford","year":"1987"},{"key":"10.1016\/0747-7171(92)90025-Y_BIB30","series-title":"Proceedings 2nd International Workshop on Algebraic and Logic Programming","first-page":"262","article-title":"Implementation of completion by transition rules + control: ORME","volume":"volume 463","author":"Lescanne","year":"1990"},{"key":"10.1016\/0747-7171(92)90025-Y_BIB31","series-title":"Unification","first-page":"393","article-title":"Adventures in associative-commutative unification","author":"Lincoln","year":"1990"},{"key":"10.1016\/0747-7171(92)90025-Y_BIB32","article-title":"Unification of bags and sets","author":"Livesey","year":"1976"},{"key":"10.1016\/0747-7171(92)90025-Y_BIB33","series-title":"Proceedings 4th Conference on Rewriting Techniques and Applications","first-page":"162","article-title":"Minimal solutions of linear diophantine systems: Bounds and algorithms","volume":"volume 488","author":"Pottier","year":"1991"},{"key":"10.1016\/0747-7171(92)90025-Y_BIB34","series-title":"Solutions of a linear diophantine system","author":"Romeuf","year":"1988"},{"key":"10.1016\/0747-7171(92)90025-Y_BIB35","doi-asserted-by":"crossref","DOI":"10.1016\/0304-3975(90)90082-S","article-title":"A polynomial algorithm for solving systems of two linear diophantine equations","author":"Romeuf","year":"1989"},{"key":"10.1016\/0747-7171(92)90025-Y_BIB36","series-title":"Unification","first-page":"217","article-title":"Unification in a combination of arbitrary disjoint equational theories","author":"Schmidt-Schau\u00df","year":"1990"},{"key":"10.1016\/0747-7171(92)90025-Y_BIB37","series-title":"Unification","first-page":"1","article-title":"Unification theory","author":"Siekmann","year":"1990"},{"key":"10.1016\/0747-7171(92)90025-Y_BIB38","series-title":"Proceedings 4th International Joint Conference on Artificial Intelligence","first-page":"71","article-title":"A complete unification algorithm for associative-commutative functions","author":"Stickel","year":"1975"},{"key":"10.1016\/0747-7171(92)90025-Y_BIB39","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":"Journal of the Association for Computing Machinery"},{"key":"10.1016\/0747-7171(92)90025-Y_BIB40","series-title":"Proceedings 1st Conference on Rewriting Techniques and Applications","first-page":"301","article-title":"Combining unification algorithm for confined equational theories","volume":"volume 202","author":"Yelick","year":"1985"}],"container-title":["Journal of Symbolic Computation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:074771719290025Y?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:074771719290025Y?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,2,1]],"date-time":"2019-02-01T00:26:50Z","timestamp":1548980810000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/074771719290025Y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1992,7]]},"references-count":40,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1992,7]]}},"alternative-id":["074771719290025Y"],"URL":"https:\/\/doi.org\/10.1016\/0747-7171(92)90025-y","relation":{},"ISSN":["0747-7171"],"issn-type":[{"value":"0747-7171","type":"print"}],"subject":[],"published":{"date-parts":[[1992,7]]}}}