{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T02:01:31Z","timestamp":1760061691336},"reference-count":55,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[1986,1,1]],"date-time":"1986-01-01T00:00:00Z","timestamp":504921600000},"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":10059,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theoretical Computer Science"],"published-print":{"date-parts":[[1986]]},"DOI":"10.1016\/0304-3975(86)90175-1","type":"journal-article","created":{"date-parts":[[2003,5,13]],"date-time":"2003-05-13T00:04:58Z","timestamp":1052784298000},"page":"189-200","source":"Crossref","is-referenced-by-count":51,"special_numbering":"C","title":["Complete sets of unifiers and matchers in equational theories"],"prefix":"10.1016","volume":"43","author":[{"given":"Fran\u00e7ois","family":"Fages","sequence":"first","affiliation":[]},{"given":"G\u00e9rard","family":"Huet","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/0304-3975(86)90175-1_bib1","article-title":"The complexity of unification","author":"Baxter","year":"1977"},{"key":"10.1016\/0304-3975(86)90175-1_bib2","doi-asserted-by":"crossref","first-page":"170","DOI":"10.1016\/S0019-9958(78)90172-9","article-title":"The undecidability of the third order dyadic unification problem","volume":"38","author":"Baxter","year":"1978","journal-title":"Inform. and Control"},{"key":"10.1016\/0304-3975(86)90175-1_bib3","series-title":"Programming in POP-2","author":"Burstall","year":"1971"},{"key":"10.1016\/0304-3975(86)90175-1_bib4","article-title":"L'anatomie de Prolog II","author":"Van Caneghem","year":"1984"},{"key":"10.1016\/0304-3975(86)90175-1_bib5","series-title":"Rappt. Int., Groupe d'Intelligence Artificielle","article-title":"Prolog II, manuel de r\u00e9f\u00e9rence et mod\u00e8le th\u00e9orique","author":"Colmerauer","year":"1982"},{"key":"10.1016\/0304-3975(86)90175-1_bib6","series-title":"Rappt. Int., GIA","article-title":"\u00c9tude et r\u00e9alisation d'un syst\u00e8me PROLOG","author":"Colmerauer","year":"1972"},{"issue":"3","key":"10.1016\/0304-3975(86)90175-1_bib7","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"},{"key":"10.1016\/0304-3975(86)90175-1_bib8","doi-asserted-by":"crossref","DOI":"10.1016\/S0747-7171(85)80027-4","article-title":"Abstract properties of substitutions and unifiers","volume":"1","author":"Eder","year":"1985","journal-title":"J. Symbolic Comput."},{"key":"10.1016\/0304-3975(86)90175-1_bib9","article-title":"Formes canoniques dans les alg\u00e8bres bool\u00e9ennes et application\u00e0la d\u00e9monstration automatique en logique de premier ordre","author":"Fages","year":"1983"},{"key":"10.1016\/0304-3975(86)90175-1_bib10_1","unstructured":"F. Fages, Associative-commutative unification, Res. REpt. LITP, Paris; submitted to J. Symbolic Comput.;"},{"key":"10.1016\/0304-3975(86)90175-1_bib10_2","series-title":"INRIA Rept. No. 287 presented at CADE'7","volume":"170","author":"Fages","year":"1984"},{"key":"10.1016\/0304-3975(86)90175-1_bib11","series-title":"Res. Rept. No. 368","article-title":"Le syste\u00e8me KB: Pr\u00e9sentation et bibliographie, mise en \u0153vre","author":"Fages","year":"1985"},{"key":"10.1016\/0304-3975(86)90175-1_bib12","series-title":"4th Workshop on Automated Deduction","first-page":"161","article-title":"First-order unification in an equational theory","author":"Fay","year":"1979"},{"key":"10.1016\/0304-3975(86)90175-1_bib13","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1016\/0304-3975(81)90040-2","article-title":"The undecidability of the second-order unification problem","volume":"13","author":"Goldfarb","year":"1981","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/0304-3975(86)90175-1_bib14","article-title":"A matching procedure for omega order logic","author":"Gould","year":"1966","journal-title":"Scient. Rept. 1, AFCRL 66-781"},{"key":"10.1016\/0304-3975(86)90175-1_bib15","article-title":"Automated logic for semi-automated mathematics","author":"Guard","year":"1964","journal-title":"Scient. Rept. 1, AFCRL 64-411"},{"key":"10.1016\/0304-3975(86)90175-1_bib16_1","article-title":"Recherches sur la th\u00e9orie de la d\u00e9monstration","author":"Herbrand","year":"1930"},{"key":"10.1016\/0304-3975(86)90175-1_bib16_2","series-title":"\u00c9crits logiques de Jacques Herbrand","author":"Herbrand","year":"1968"},{"key":"10.1016\/0304-3975(86)90175-1_bib17","article-title":"Topics in automated theorem proving and program generation","author":"Hsiang","year":"1982"},{"key":"10.1016\/0304-3975(86)90175-1_bib18","doi-asserted-by":"crossref","first-page":"257","DOI":"10.1016\/S0019-9958(73)90301-X","article-title":"The undecidability of unification in third-order logic","volume":"22","author":"Huet","year":"1973","journal-title":"Inform. and Control"},{"issue":"1","key":"10.1016\/0304-3975(86)90175-1_bib19","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1016\/0304-3975(75)90011-0","article-title":"A unification algorithm for typed \u03bb-calculus","volume":"1","author":"Huet","year":"1975","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/0304-3975(86)90175-1_bib20","article-title":"R\u00e9solution d'\u00e9quations dans des langages d'ordre 1,2,..., \u03c9","author":"Huet","year":"1976"},{"issue":"3","key":"10.1016\/0304-3975(86)90175-1_bib21","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 homogeneous, linear Diophantine equations","volume":"7","author":"Huet","year":"1978","journal-title":"Inform. Process. Lett."},{"key":"10.1016\/0304-3975(86)90175-1_bib22","series-title":"Formal Languages: Perspectives and Open Problems","article-title":"Equations and rewrite rules: A survey","author":"Huet","year":"1980"},{"key":"10.1016\/0304-3975(86)90175-1_bib23","article-title":"Compilation de formes canoniques dans les th\u00e9ories\u00e9quationnelles","author":"Hullot","year":"1980"},{"key":"10.1016\/0304-3975(86)90175-1_bib24","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1016\/0304-3975(76)90021-9","article-title":"Mechanizing \u03c9-order type theory through unification","volume":"3","author":"Jensen","year":"1977","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/0304-3975(86)90175-1_bib25","series-title":"Proc. 10th ICALP","article-title":"Incremental construction of unification algorithms in equational theories","author":"Jouannaud","year":"1983"},{"key":"10.1016\/0304-3975(86)90175-1_bib26","series-title":"Proc. Rewrite Techniques and Applications","first-page":"417","article-title":"Complexity of matching problem","volume":"202","author":"Kapur","year":"1985"},{"key":"10.1016\/0304-3975(86)90175-1_bib27","article-title":"Contribution\u00e0la r\u00e9solution d'\u00e9quations dans les alg\u00e8bres libres et les vari\u00e9tes\u00e9quationnelles d'alg\u00e8bres","author":"Kirchner","year":"1982"},{"key":"10.1016\/0304-3975(86)90175-1_bib28","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\/0304-3975(86)90175-1_bib29","series-title":"Computational Problems in Abstract Algebra","first-page":"263","article-title":"Simple word problems in universal algebras","author":"Knuth","year":"1970"},{"key":"10.1016\/0304-3975(86)90175-1_bib30","series-title":"Rept. MTP-1","article-title":"A unification algorithm for Abelian group theory","author":"Lankford","year":"1979"},{"key":"10.1016\/0304-3975(86)90175-1_bib31","series-title":"Abelian group unification algorithms for elementary terms","author":"Lankford","year":"1983"},{"key":"10.1016\/0304-3975(86)90175-1_bib32","series-title":"Int. Rept. 3\/76","article-title":"Unification of bags and sets","author":"Livesey","year":"1976"},{"key":"10.1016\/0304-3975(86)90175-1_bib33","series-title":"4th Workshop on Automated Deduction","first-page":"161","article-title":"Unification problems for combinations of associativity, commutativity, distributivity and idempotence axioms","author":"Livesey","year":"1979"},{"issue":"2","key":"10.1016\/0304-3975(86)90175-1_bib34","first-page":"287","article-title":"The problem of solvability of equations in a free semigroup","volume":"23","author":"Makanin","year":"1977","journal-title":"Akad. Nauk. SSSR. TOM"},{"issue":"2","key":"10.1016\/0304-3975(86)90175-1_bib35","doi-asserted-by":"crossref","first-page":"258","DOI":"10.1145\/357162.357169","article-title":"An efficient unification algorithm","volume":"4","author":"Martelli","year":"1982","journal-title":"ACM TOPLAS"},{"key":"10.1016\/0304-3975(86)90175-1_bib36","series-title":"Proc. 2nd Scandinavian Logic Symposium","article-title":"Diophantine representation of recursively enumerable predicates","author":"Matiyasevich","year":"1970"},{"key":"10.1016\/0304-3975(86)90175-1_bib37","doi-asserted-by":"crossref","first-page":"158","DOI":"10.1016\/0022-0000(78)90043-0","article-title":"Linear unification","volume":"16","author":"Paterson","year":"1978","journal-title":"J. Comput. System Sci."},{"issue":"2","key":"10.1016\/0304-3975(86)90175-1_bib38","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":"J. ACM"},{"key":"10.1016\/0304-3975(86)90175-1_bib39","first-page":"73","article-title":"Building-in equational theories","volume":"7","author":"Plotkin","year":"1972","journal-title":"Machine Intelligence"},{"key":"10.1016\/0304-3975(86)90175-1_bib40","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 Bull. 1979"},{"key":"10.1016\/0304-3975(86)90175-1_bib41","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":"J. ACM"},{"key":"10.1016\/0304-3975(86)90175-1_bib42","first-page":"135","article-title":"Paramodulation and theorem proving in first-order theories with equality","volume":"4","author":"Robinson","year":"1969","journal-title":"Machine Intelligence"},{"key":"10.1016\/0304-3975(86)90175-1_bib43","series-title":"Tech. Note 73","article-title":"QA4: A procedural calculus for intuitive reasoning","author":"Rulifson","year":"1972"},{"key":"10.1016\/0304-3975(86)90175-1_bib44","series-title":"Memo CSM-4-78","article-title":"Unification and matching problems","author":"Siekmann","year":"1978"},{"key":"10.1016\/0304-3975(86)90175-1_bib45","series-title":"6th CADE","article-title":"Universal unification in regular equational ACFM theories","author":"Siekmann","year":"1982"},{"key":"10.1016\/0304-3975(86)90175-1_bib46","doi-asserted-by":"crossref","first-page":"622","DOI":"10.1145\/321850.321859","article-title":"Automated theorem-proving for theories with simplifiers, commutativity and associativity","volume":"21","author":"Slagle","year":"1974","journal-title":"J. ACM"},{"key":"10.1016\/0304-3975(86)90175-1_bib47","series-title":"4th Internat. Joint Conf. on Artificial Intelligence","article-title":"A complete unification algorithm for associative-commutative functions","author":"Stickel","year":"1975"},{"key":"10.1016\/0304-3975(86)90175-1_bib48","article-title":"Unification algorithms for artificial intelligence languages","author":"Stickel","year":"1976"},{"issue":"3","key":"10.1016\/0304-3975(86)90175-1_bib49","doi-asserted-by":"crossref","first-page":"423","DOI":"10.1145\/322261.322262","article-title":"A complete unification algorithm for associative-commutative functions","volume":"28","author":"Stickel","year":"1981","journal-title":"J. ACM"},{"issue":"IV","key":"10.1016\/0304-3975(86)90175-1_bib50","doi-asserted-by":"crossref","first-page":"361","DOI":"10.1007\/BF02575754","article-title":"Complexity of the unification algorithm for first-order expressions","volume":"XII","author":"Venturini Zilli","year":"1975","journal-title":"Calcolo"},{"key":"10.1016\/0304-3975(86)90175-1_bib51","article-title":"Unification in combinations of theories with disjoint sets of function symbols","author":"Tiden","year":"1985","journal-title":"Royal Inst. of Technology, Dept. of Computer Science, S-100 44"},{"key":"10.1016\/0304-3975(86)90175-1_bib52","series-title":"Combining unification algorithms for confined equational theories","author":"Yellick","year":"1985"},{"key":"10.1016\/0304-3975(86)90175-1_bib53","article-title":"Computational logic: The unification computation","volume":"Vol. 6","author":"Robinson","year":"1971"}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:0304397586901751?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:0304397586901751?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,3,21]],"date-time":"2019-03-21T08:53:05Z","timestamp":1553158385000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/0304397586901751"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1986]]},"references-count":55,"alternative-id":["0304397586901751"],"URL":"https:\/\/doi.org\/10.1016\/0304-3975(86)90175-1","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[1986]]}}}