{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:02:25Z","timestamp":1725663745902},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540525318"},{"type":"electronic","value":"9783540470144"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1990]]},"DOI":"10.1007\/3-540-52531-9_137","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T21:35:51Z","timestamp":1330205751000},"page":"174-183","source":"Crossref","is-referenced-by-count":1,"title":["AC-unification race: The system solving approach and its implementation"],"prefix":"10.1007","author":[{"given":"Mohamed","family":"Adi","sequence":"first","affiliation":[]},{"given":"Claude","family":"Kirchner","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,5]]},"reference":[{"key":"20_CR1","unstructured":"M. Adi and C. Kirchner. AC-Unification Race: the System Solving Approach, Implementation and Benchmarks. Research Report 89-R-169, CRIN, Nancy (France), 1989."},{"key":"20_CR2","unstructured":"A. Boudet. A new Combination Technique for AC Unification. Internal Report 494, LRI, Orsay (France), June 1989."},{"issue":"1","key":"20_CR3","doi-asserted-by":"crossref","first-page":"465","DOI":"10.1007\/BF00297251","volume":"4","author":"H-J. B\u00fcrckert","year":"1988","unstructured":"H-J. B\u00fcrckert, A. Herold, D. Kapur, J. Siekmann, M. Stickel, M. Tepp, and H. Zhang. Opening the AC-unification race. Journal of Automated Reasoning, 4(1):465\u2013474, 1988.","journal-title":"Journal of Automated Reasoning"},{"issue":"1&2","key":"20_CR4","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/S0747-7171(89)80021-5","volume":"8","author":"H-J. B\u00fcrckert","year":"1989","unstructured":"H-J. B\u00fcrckert, A. Herold, and M. Schmidt-Schau\u00df. On equational theories, unification and decidability. Journal of Symbolic Computation, 8(1 & 2):3\u201350, 1989. Special issue on unification. Part two.","journal-title":"Journal of Symbolic Computation"},{"issue":"1&2","key":"20_CR5","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1016\/S0747-7171(89)80025-2","volume":"8","author":"M Clausen","year":"1989","unstructured":"M Clausen and A. Fortenbacher. Efficient solution of linear diophantine equations. Journal of Symbolic Computation, 8(1 & 2):201\u2013216, 1989. Special issue on unification. Part two.","journal-title":"Journal of Symbolic Computation"},{"key":"20_CR6","unstructured":"E. Domenjoud. AC unification through order-sorted AC1 unification. In H-J. B\u00fcrckert and W. Nutt, editors, Proceedings of UNIF'89, third international workshop on unification, Lambrecht (FR Germany), June 1989. Also in CRIN Research Report 89-R-67."},{"key":"20_CR7","unstructured":"E. Domenjoud. Number of Minimal Unifiers of the Equation \u03b1x\n1 + ... + \u03b1x\np =AC \u03b2y1 + ... + \u03b2yq. Research Report 89-R-2, CRIN, Nancy (France), 1989. To appear in the Journal of Automated Reasoning (1990)."},{"key":"20_CR8","unstructured":"H. Devie E. Contejean. Solving systems of linear diophantine equations. In H-J. B\u00fcrckert and W. Nutt, editors, Proceedings of UNIF'89, third international workshop on unification, Lambrecht (FR Germany), June 1989."},{"issue":"1","key":"20_CR9","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1016\/0304-3975(86)90175-1","volume":"43","author":"F. Fages","year":"1986","unstructured":"F. Fages and G. Huet. Complete sets of unifiers and matchers in equational theories. Theoretical Computer Science, 43(1):189\u2013200, 1986.","journal-title":"Theoretical Computer Science"},{"key":"20_CR10","unstructured":"A Fortenbacher. Algebraische unifikation. 1983. Diplomarbeit, Institut f\u00fcr Informatik, Universit\u00e4t Karlsruhe."},{"key":"20_CR11","unstructured":"A. Herold. Combination of Unification Algorithms in Equational Theories. PhD thesis, Universit\u00e4t Kaiserslautern, 1987."},{"issue":"3","key":"20_CR12","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(3):144\u2013147, 1978.","journal-title":"Information Processing Letters"},{"key":"20_CR13","volume-title":"Compilation de formes canoniques dans les th\u00e9ories \u00e9quationelles","author":"J-M. Hullot","year":"1980","unstructured":"J-M. Hullot. Compilation de formes canoniques dans les th\u00e9ories \u00e9quationelles. Th\u00e8se de 3i\u00e8me cycle, Universit\u00e9 de Paris Sud, Orsay, France, 1980."},{"key":"20_CR14","doi-asserted-by":"crossref","unstructured":"D. Kapur and P. Narendran. NP-completeness of the set unification and matching problems. In J. Siekmann, editor, Proceedings 8th Conference on Automated Deduction, Springer-Verlag, 1986.","DOI":"10.1007\/3-540-16780-3_113"},{"key":"20_CR15","first-page":"171","volume-title":"Resolution of Equations in Algebraic Structures","author":"C. Kirchner","year":"1989","unstructured":"C. Kirchner. From unification in combination of equational theories to a new AC-unification algorithm. In H. A\u00eft-Kaci and M. Nivat, editors, Resolution of Equations in Algebraic Structures, pages 171\u2013210, Academic Press, New-York, 1989."},{"key":"20_CR16","unstructured":"C. Kirchner. M\u00e9thodes et outils de conception syst\u00e9matique d'algorithmes d'unification dans les th\u00e9ories \u00e9quationnelles. Th\u00e8se d'\u00e9tat de l'Universit\u00e9 de Nancy I, 1985."},{"key":"20_CR17","unstructured":"C. Kirchner. Methods and tools for equational unification. In Proceedings of the Colloquium on Resolution of Equations in Algebraic Structures, Austin (Texas), May 1987."},{"issue":"1","key":"20_CR18","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(1):39\u201340, 1987.","journal-title":"Compte-rendu de L'Acad\u00e9mie des Sciences de Paris"},{"key":"20_CR19","volume-title":"Non-negative integer basis algorithms for linear equations with integer coefficients","author":"D. Lankford","year":"1987","unstructured":"D. Lankford. Non-negative integer basis algorithms for linear equations with integer coefficients. Technical Report, Louisiana Tech University, Ruston, LA 71272, 1987."},{"issue":"1&2","key":"20_CR20","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1016\/S0747-7171(89)80026-4","volume":"8","author":"P. Lincoln","year":"1989","unstructured":"P. Lincoln and J. Christian. Adventures in associative-commutative unification. Journal of Symbolic Computation, 8(1 & 2):217\u2013240, 1989. Special issue on unification. Part two.","journal-title":"Journal of Symbolic Computation"},{"key":"20_CR21","unstructured":"M. Livesey and J. Siekmann. Unification of Bags and Sets. Technical Report, Institut fur Informatik I, Universit\u00e4t Karlsruhe, 1976."},{"key":"20_CR22","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1145\/322248.322251","volume":"28","author":"G. Peterson","year":"1981","unstructured":"G. Peterson and M. Stickel. Complete sets of reductions for some equational theories. Journal of the Association for Computing Machinery, 28:233\u2013264, 1981.","journal-title":"Journal of the Association for Computing Machinery"},{"key":"20_CR23","unstructured":"J.-F. Romeuf. A polynomial algorithm for solving systems of two linear diophantine equations. Technical Report, Laboratoire d'Informatique de Rouen (France) and LITP, 1989."},{"issue":"1&2","key":"20_CR24","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1016\/S0747-7171(89)80022-7","volume":"8","author":"M. Schmidt-Schauss","year":"1989","unstructured":"M. Schmidt-Schauss. Combination of unification algorithms. Journal of Symbolic Computation, 8(1 & 2):51\u2013100, 1989. Special issue on unification. Part two.","journal-title":"Journal of Symbolic Computation"},{"key":"20_CR25","doi-asserted-by":"crossref","first-page":"423","DOI":"10.1145\/322261.322262","volume":"28","author":"M.E. Stickel","year":"1981","unstructured":"M.E. Stickel. A unification algorithm for associative-commutative functions. Journal of the Association for Computing Machinery, 28:423\u2013434, 1981.","journal-title":"Journal of the Association for Computing Machinery"},{"key":"20_CR26","unstructured":"M.E. Stickel. Unification Algorithms for Artificial Intelligence Languages. PhD thesis, Carnegie-mellon University, 1976."},{"key":"20_CR27","first-page":"301","volume-title":"Proceedings of the 1st Conference on Rewriting Techniques and Applications","author":"K. Yelick","year":"1985","unstructured":"K. Yelick. Combining unification algorithm for confined equational theories. In J.-P. Jouannaud, editor, Proceedings of the 1st Conference on Rewriting Techniques and Applications, pages 301\u2013324, Springer-Verlag, Dijon (France), May 1985."}],"container-title":["Lecture Notes in Computer Science","Design and Implementation of Symbolic Computation Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-52531-9_137.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,28]],"date-time":"2021-04-28T01:08:18Z","timestamp":1619572098000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-52531-9_137"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1990]]},"ISBN":["9783540525318","9783540470144"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/3-540-52531-9_137","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1990]]}}}