{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,22]],"date-time":"2025-03-22T04:17:08Z","timestamp":1742617028451,"version":"3.40.2"},"publisher-location":"Berlin, Heidelberg","reference-count":35,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540127277"},{"type":"electronic","value":"9783540387145"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1983]]},"DOI":"10.1007\/3-540-12727-5_12","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T17:54:31Z","timestamp":1330192471000},"page":"205-220","source":"Crossref","is-referenced-by-count":22,"title":["Complete sets of unifiers and matchers in equational theories"],"prefix":"10.1007","author":[{"given":"Fran\u00e7ois","family":"Fages","sequence":"first","affiliation":[]},{"given":"G\u00e9rard","family":"Huet","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,29]]},"reference":[{"key":"12_CR1","unstructured":"Baxter L.D. The Complexity of Unification. Ph. D. Thesis, University of Waterloo. (1977)"},{"key":"12_CR2","doi-asserted-by":"publisher","first-page":"170","DOI":"10.1016\/S0019-9958(78)90172-9","volume":"38","author":"L. D. Baxter","year":"1978","unstructured":"Baxter L.D. The Undecidability of the Third Order Dyadic Unification Problem. Information and Control 38, p170\u2013178, (1978)","journal-title":"Information and Control"},{"key":"12_CR3","unstructured":"Colmerauer A. Un syst\u00e8me de communication homme-machine en Fran\u00e7ais. Rapport pr\u00e9liminaire, Groupe de recherche en Intelligence Artificielle, U.E.R. de Luminy, Univ. d'Aix-Marseille. (octobre 1972)"},{"key":"12_CR4","unstructured":"Colmerauer A. Prolog II, manuel de r\u00e9f\u00e9rence et mod\u00e8le th\u00e9orique. Rapport interne, Groupe d'Intelligence Artificielle, Univ. d'Aix-Marseille II. (Mars 1982)"},{"key":"12_CR5","unstructured":"Fay M. First-order Unification in an Equational Theory. 4th Workshop on Automated Deduction, Austin, Texas, pp. 161\u2013167. (Feb. 1979)"},{"key":"12_CR6","doi-asserted-by":"crossref","unstructured":"Goldfarb W. The Undecidability of the Second-Order Unification Problem. Theoritical Computer Science 13, pp 225\u2013230. North Holland Publishing Company. (1981)","DOI":"10.1016\/0304-3975(81)90040-2"},{"key":"12_CR7","unstructured":"Gould W.E. A matching Procedure for Omega Order Logic. Scientific Report 1, AFCRL 66\u2013781, contract AF19 (628)\u20133250. (1966)"},{"key":"12_CR8","unstructured":"Guard J.R. Automated Logic for Semi-Automated Mathematics, Scientific Report 1, AFCRL 64, 411, Contract AF19 (628)\u20133250. (1964)"},{"key":"12_CR9","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1145\/321495.321500","volume":"16","author":"J. R. Guard","year":"1969","unstructured":"Guard J.R., Oglesby F.C., Bennett J.H. and Settle L.G. Semi-automated Mathematics. JACM 16, pp. 49\u201362. (1969)","journal-title":"JACM"},{"key":"12_CR10","doi-asserted-by":"crossref","unstructured":"Herbrand J. Recherches sur la th\u00e9orie de la d\u00e9monstration. Th\u00e8se, U. de Paris, In: Ecrits logiques de Jacques Herbrand, PUF Paris 1968. (1930)","DOI":"10.3917\/puf.herbr.1968.01.0031"},{"key":"12_CR11","unstructured":"Hsiang J. Topics in Automated Theorem Proving and Program Generation. Ph. D. Thesis, Univ. of Illinois at Urbana-Champaign. (Nov. 1982)"},{"key":"12_CR12","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1016\/S0019-9958(73)90301-X","volume":"22","author":"G. Huet","year":"1973","unstructured":"Huet G. The Undecidability of Unification in Third Order Logic. Information and Control 22, pp 257\u2013267. (1973)","journal-title":"Information and Control"},{"key":"12_CR13","unstructured":"Huet G. R\u00e9solution d'\u00e9quations dans des langages d'ordre 1, 2, ... omega. Th\u00e8se d'Etat, Univ. de Paris VII. (1976)"},{"key":"12_CR14","doi-asserted-by":"crossref","unstructured":"Huet G. and Oppen D. Equations and Rewrite Rules: a Survey. In Formal Languages: Perspectives and Open Problems, Ed. Book R., Academic Press. (1980)","DOI":"10.1016\/B978-0-12-115350-2.50017-8"},{"key":"12_CR15","unstructured":"Hullot J.M. Compilation de Formes Canoniques dans les Th\u00e9ories Equationnelles. Th\u00e8se de 3\u00e8me cycle. U. de Paris Sud. (Nov. 1980)"},{"key":"12_CR16","unstructured":"Kirchner C. and Kirchner H. Contribution \u00e0 la r\u00e9solution d'\u00e9quations dans les alg\u00e8bres libres et les vari\u00e9t\u00e9s \u00e9quationnelles d'alg\u00e8bres. Th\u00e8se de 3\u00e8me cycle, Univ. de Nancy. (Mars 1982)"},{"key":"12_CR17","doi-asserted-by":"crossref","unstructured":"Knuth D. and Bendix P. Simple Word Problems in Universal Algebras. In Computational Problems in Abstract Algebra, Ed. Leech J., Pergamon Press, pp. 263\u2013297. (1970)","DOI":"10.1016\/B978-0-08-012975-4.50028-X"},{"key":"12_CR18","unstructured":"Lankford D.S. A Unification Algorithm for Abelian Group Theory. Report MTP-1, Math. Dept., Louisiana Tech. U. (Jan. 1979)"},{"key":"12_CR19","unstructured":"Livesey M. and Siekmann J. Unification of bags and sets. Internal Report 3|76, Institut fur Informatik I, U. Karlsruhe, (1976)"},{"key":"12_CR20","first-page":"233","volume":"2","author":"G. S. Makanin","year":"1977","unstructured":"Makanin G.S. The Problem of Solvability of Equations in a Free Semigroup. Akad. Nauk. SSSR, TOM pp. 233, 2. (1977)","journal-title":"Akad. Nauk. SSSR, TOM"},{"issue":"2","key":"12_CR21","first-page":"258","volume":"4","author":"A. Martelli","year":"1982","unstructured":"Martelli A. and Montanari U. An Efficient Unification Algorithm. ACM T.O.P.L.A.S., Vol. 4, No. 2, pp 258\u2013282. (April 1982)","journal-title":"ACM T.O.P.L.A.S."},{"key":"12_CR22","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1016\/0022-0000(78)90043-0","volume":"16","author":"M. S. Paterson","year":"1978","unstructured":"Paterson M.S. and Wegman M.N. Linear Unification. J. of Computer and Systems Sciences 16, pp. 158\u2013167. (1978)","journal-title":"J. of Computer and Systems Sciences"},{"issue":"2","key":"12_CR23","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1145\/322248.322251","volume":"28","author":"G. E. Peterson","year":"1981","unstructured":"Peterson G.E. and Stickel M.E. Complete Sets of Reduction for Equational Theories with Complete Unification Algorithms. JACM 28, 2 pp 233\u2013264. (1981)","journal-title":"JACM"},{"key":"12_CR24","first-page":"73","volume":"7","author":"G. Plotkin","year":"1972","unstructured":"Plotkin G. Building-in Equational Theories. Machine Intelligence 7, pp. 73\u201390. (1972)","journal-title":"Machine Intelligence"},{"key":"12_CR25","unstructured":"Robinson G.A. and Wos L.T. Paramodulation and Theorem Proving in First-order Theories with Equality. Machine Intelligence 4, American Elsevier, pp. 135\u2013150. (1969)"},{"key":"12_CR26","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1145\/321250.321253","volume":"12","author":"J. A. Robinson","year":"1965","unstructured":"Robinson J.A. A Machine-Oriented Logic Based on the Resolution Principle. JACM 12, pp. 32\u201341. (1965)","journal-title":"JACM"},{"key":"12_CR27","volume-title":"Computational Logic: the Unification Computation. Machine Intelligence 6","author":"J. A. Robinson","year":"1971","unstructured":"Robinson J.A. Computational Logic: the Unification Computation. Machine Intelligence 6, Eds B. Meltzer and D. Michie American Elsevier, New-York. (1971)"},{"key":"12_CR28","unstructured":"Rulifson J.F., Derksen J.A. and Waldinger R.J. QA4: a Procedural Calculus for Intuitive Reasoning. Technical Note 73, Artificial Intelligence Center, Stanford Research Institute, Menlo Park, California. (November 1972)"},{"key":"12_CR29","unstructured":"Siekmann J. Unification and Matching Problems. Ph. D. Thesis, Univ. Karlsruhe. (March 1978)"},{"key":"12_CR30","doi-asserted-by":"crossref","unstructured":"Siekmann J. and Szabo P. Universal Unification in Regular Equational ACFM Theories. CADE 6th, New-York. (June 1982)","DOI":"10.1007\/978-3-642-68826-3_9"},{"key":"12_CR31","doi-asserted-by":"publisher","first-page":"622","DOI":"10.1145\/321850.321859","volume":"21","author":"J. R. Slagle","year":"1974","unstructured":"Slagle J.R. Automated Theorem-Proving for Theories with Simplifiers, Commutativity and Associativity JACM 21, pp. 622\u2013642. (1974)","journal-title":"JACM"},{"issue":"3","key":"12_CR32","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1145\/322261.322262","volume":"28","author":"M. E. Stickel","year":"1981","unstructured":"Stickel M.E. A Complete Unification Algorithm for Associative-Commutative Functions. JACM 28, 3 pp. 423\u2013434. (1981)","journal-title":"JACM"},{"key":"12_CR33","doi-asserted-by":"crossref","unstructured":"Stickel M.E. A Complete Unification Algorithm for Associative-Commutative Functions. 4th International Joint Conference on Artificial Intelligence, Tbilisi. (1975)","DOI":"10.21236\/ADA015846"},{"key":"12_CR34","unstructured":"Stickel M.E. Unification Algorithms for Artificial Intelligence Languages. Ph. D. Thesis, Carnegie-Mellon University. (1976)"},{"key":"12_CR35","doi-asserted-by":"crossref","first-page":"361","DOI":"10.1007\/BF02575754","volume":"IV","author":"M. Venturini-Zilli","year":"1975","unstructured":"Venturini-Zilli M. Complexity of the Unification Algorithm for First-Order Expressions. Calcolo XII, Fasc. IV, p 361\u2013372. (1975)","journal-title":"Calcolo XII, Fasc."}],"container-title":["Lecture Notes in Computer Science","CAAP'83"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-12727-5_12.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T20:18:10Z","timestamp":1742588290000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-12727-5_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1983]]},"ISBN":["9783540127277","9783540387145"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/3-540-12727-5_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1983]]}}}