{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,14]],"date-time":"2025-07-14T02:45:27Z","timestamp":1752461127653,"version":"3.38.0"},"publisher-location":"New York, NY","reference-count":50,"publisher":"Springer New York","isbn-type":[{"type":"print","value":"9780387960227"},{"type":"electronic","value":"9780387347684"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1984]]},"DOI":"10.1007\/978-0-387-34768-4_12","type":"book-chapter","created":{"date-parts":[[2011,5,9]],"date-time":"2011-05-09T04:01:06Z","timestamp":1304913666000},"page":"194-208","source":"Crossref","is-referenced-by-count":30,"title":["Associative-Commutative Unification"],"prefix":"10.1007","author":[{"given":"Fran\u00e7ois","family":"Fages","sequence":"first","affiliation":[]}],"member":"297","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 Control 38, p 170\u2013178, (1978)","journal-title":"Information Control"},{"key":"12_CR3","unstructured":"Burstall R.M., Colli. J.S. and Popplestone R.J. Programming in POP-2 Edinburgh University Press. (1971)"},{"key":"12_CR4","unstructured":"Colmerauer A. Prolog II, manuel de r\u00e9f\u00e9rence et mod\u00e8le th\u00e9orique, Rapport interne, Groupe d\u2019Intelligence Artificielle, Universit\u00e9 d\u2019Aix-Marseille II. (Mars 1982)"},{"key":"12_CR5","unstructured":"Colmerauer K. Kanoui H. and Van Caneghem M. Etude et R\u00e9alisation d\u2019un syst\u00e9me PROLOG. Rapport Interne, GIA, Univ. d\u2019Aix-MarseiUe Luminy. (1972)"},{"issue":"3","key":"12_CR6","doi-asserted-by":"publisher","first-page":"233","DOI":"10.2307\/2318447","volume":"80","author":"M. Davis","year":"1973","unstructured":"Davis M. Hilbert\u2019s Tenth Problem is Unsolvable. Amer. Math. Monthly 80,3, pp. 233\u2013289. (1973)","journal-title":"Amer. Math. Monthly"},{"key":"12_CR7","unstructured":"Fages F. Formes canoniques dons les alg\u00e8bres bool\u00e9ennes, et application \u00e0 la d\u00e9monstration automatique en logique de premier ordre. Th\u00e8se, Universit\u00e9 de Paris VI. (June 83)"},{"key":"12_CR8","unstructured":"Fages F. Note sur l\u2019unification des termes de premier ordre finis et infinis. Rapport LITP 83-29. (May 1983)"},{"key":"12_CR9","unstructured":"Fages F. and Huet G. Unification and Matching in Equational Theories. CAAP 83, l\u2019Aquila, Italy. Lecture Notes in Computer Science 159. (March 1983)"},{"key":"12_CR10","unstructured":"Fay M. First-order Unification in an Equational Theory. 4th Workshop on Automated Deduction, Austin, Texas, pp. 161\u2013167. (Feb. 1979)"},{"key":"12_CR11","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1016\/0304-3975(81)90040-2","volume":"13","author":"W.D. Goldfarb","year":"1981","unstructured":"Goldfarb W.D. The Undecidability of the Second-order Unification Problem. Theoritical Computer Science, vol. 13, pp. 225\u2013230. North Holland Publishing Company. (1981)","journal-title":"Theoritical Computer Science"},{"key":"12_CR12","doi-asserted-by":"crossref","unstructured":"Gordon M.J., Milner A.J. and Wadmworth C.P. Edinburgh LCF. Springer-Verlag LNCS 78. (1979)","DOI":"10.1007\/3-540-09724-4"},{"key":"12_CR13","unstructured":"Gould W.E. A Matching Procedure for Omega Order Logic. Scientific Report 1, AFCRL 66-781, contract AF 19 (628)-3250, (1966)"},{"key":"12_CR14","unstructured":"Guard J.R. Automated Logic for Semi-Automated Mathematics. Scientific Report 1, AFCRL 64,411, Contract AF 19 (628)-3250.(1964)"},{"key":"12_CR15","doi-asserted-by":"crossref","unstructured":"Herbrand J. Recherehes 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_CR16","unstructured":"Hsiang J. Topics in Automated Theorem Proving and Program Generation. Ph.D. Thesis, Univ. of Illinois at Urbana-Champaign. (Nov. 1982)"},{"key":"12_CR17","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_CR18","doi-asserted-by":"crossref","unstructured":"Huet G. A Unification Algorithm for Typed \u03bb-Calculus. Theoretical Computer Science 1.1, pp. 27\u201357. (1975)","DOI":"10.1016\/0304-3975(75)90011-0"},{"key":"12_CR19","unstructured":"Huet G. R\u00e9solution d\u2019\u00e9quations dons des langages d\u2019ordre 1,2..., omega. Th\u00e8se d\u2019Etat, Universit\u00e9 de Paris VII, (1976)"},{"issue":"3","key":"12_CR20","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1016\/0020-0190(78)90078-9","volume":"7","author":"G. Huet","year":"1978","unstructured":"Huet G. An Algorithm to Generate the Basis of Solutions to Homogenous Linear Diophantine Equations. Information Processing Letters 7,3, pp. 144\u2013147) (1978)","journal-title":"Information Processing Letters"},{"key":"12_CR21","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_CR22","unstructured":"Hullot J.M. Associative-Commutative Pattern Matching, Fifth International Joint Conference on Artificial Intelligence, Tokyo. (1979)"},{"key":"12_CR23","unstructured":"Huller J.M. Compilation de Formes Canoniques dons les Th\u00e9ories Equationnelles. Th\u00e8se de 3\u00e8me cycle, U. de Paris Sud. (Nov. 80)"},{"key":"12_CR24","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1016\/0304-3975(76)90021-9","volume":"3","author":"D. Jensen","year":"1977","unstructured":"Jensen D. and Pietrzykowski T. Mecanizing \u03c9-Order Type Theory through Unification, Theoretical Computer Science 3, pp. 123\u2013171. (1977)","journal-title":"Theoretical Computer Science"},{"key":"12_CR25","unstructured":"Jouannaud J.P. and Kirchner C. Incremental Construction of Unification Algorithms in Equational Theories. Proc 10th ICALP. (1983)"},{"key":"12_CR26","unstructured":"Kirchner H. and Kirchner C. Contribution \u00e0 la r\u00e9solution d\u2019\u00e9quations dons les alg\u00e8bres fibres et les vari\u00e9t\u00e9s \u00e9quationnelles d\u2019alg\u00e8bres. Th\u00e8se de 3\u00e8me cycle, Universit\u00e9 de Nancy. (Mars 1982)"},{"key":"12_CR27","doi-asserted-by":"crossref","unstructured":"Knuth D. and Bendix P. Simple Word Problems in Universal Algebras. In Computational Problems in Abstract Algebra, Pergamon Press, pp. 263\u2013297. (1970)","DOI":"10.1016\/B978-0-08-012975-4.50028-X"},{"key":"12_CR28","doi-asserted-by":"crossref","unstructured":"Landin P.J. The Next 700 Programming Languages. CACM 9,3. (March 1988)","DOI":"10.1145\/365230.365257"},{"key":"12_CR29","unstructured":"Lankford D.S. A Unification Algorithm for Abelian Group Theory. Report MTP-1, Math. Dept., Louisiana Tech. U. (Jan. 1979)"},{"key":"12_CR30","doi-asserted-by":"crossref","unstructured":"Lankford D.S., Butler G. and Brady B. Abelian Group Unification Algorithms for Elementary Terms. Math. Dept., Louisiana Tech. U., Ruston Louisiana 71272 (1983)","DOI":"10.1090\/conm\/029\/749246"},{"key":"12_CR31","unstructured":"Livesey M. and Siekmann J. Unification. of Bags and Sets. Internal Report 3\/76, Institut fur Informatik I, U. Karlsruhe. (1976)"},{"key":"12_CR32","unstructured":"Livesey M., Siekmann J., Szabo P. and Unvericht E. Unification Problems for Combinations of Associativity, Commutativity, Distributivity and Idempotence Axioms. 4th Workshop on Automated Deduction, Austin, Texas, pp. 161\u2013167. (Feb. 1979)"},{"key":"12_CR33","doi-asserted-by":"crossref","unstructured":"Makanin G.S. The Problem of Solvability of Equations in a Free Semigroup. Akad. Nauk. SSSR, TOM pp. 233,2. (1977)","DOI":"10.1070\/SM1977v032n02ABEH002376"},{"key":"12_CR34","doi-asserted-by":"crossref","unstructured":"Martelli A. and Montanari U. An Efficient Unification Algorithm. ACM T.O.P.L.A.S., Vet. 4, No. 2, pp 258\u2013282. (April 1982)","DOI":"10.1145\/357162.357169"},{"key":"12_CR35","doi-asserted-by":"crossref","unstructured":"Matiyasevich Y. Diophantine Representation of Recursively Enumerable Predicates. Proceedings of the Second Scandinavian Logic Symposium, North-Holland, (1970)","DOI":"10.1016\/S0049-237X(08)70846-2"},{"key":"12_CR36","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_CR37","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_CR38","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_CR39","doi-asserted-by":"crossref","unstructured":"Raulefs P., Siekmann J., Szabo P., Unvericht E. A Short Survey on the State of the Art in Matching and Unification Problems. Sigsam Bulletin 1979, Vol. 13. (1979)","DOI":"10.1145\/1089208.1089210"},{"key":"12_CR40","doi-asserted-by":"crossref","unstructured":"Reynolds John C. GEDANKEN \u2014 A Simple Typeless Language Based on the Principle of Completeness and the Reference Concept. CACM 13,5, pp. 308\u2013319. (May 1970)","DOI":"10.1145\/362349.362364"},{"key":"12_CR41","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1145\/321250.321253","volume":"12","author":"J. A. 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_CR42","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. (1989)"},{"key":"12_CR43","unstructured":"Rulifson J.F., Derksen J.A. and Waldinger R.J. QA4: a Procedural Calculus for Intuitive Reasoning. Technical Note 73, A.I. Center, SRI Menlo Park. (Nov. 1972)"},{"key":"12_CR44","unstructured":"Siekmann J. Unification and Matching Problems. Ph. P. thesis, Memo CSM-4-78, University of Essex, (1978)"},{"key":"12_CR45","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_CR46","doi-asserted-by":"publisher","first-page":"622","DOI":"10.1145\/321850.321859","volume":"21","author":"J.R. Siagle","year":"1974","unstructured":"Siagle J.R. Automated Theorem-Proving for Theories with Simplifiers, Commutativity and Associativity. JACM 21, pp. 622\u2013642. (1974)","journal-title":"JACM"},{"key":"12_CR47","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_CR48","unstructured":"Stickel M.E. Unification Algorithms for Artificial Intelligence Languages. Ph. D. thesis, Carnegie-Mellon University. (1976)"},{"issue":"3","key":"12_CR49","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_CR50","doi-asserted-by":"crossref","unstructured":"Venturini-Zilli M. Complexity of the Unification Algorithm for First-Order Expressions. Calcola XII, Fasc. IV, p361\u2013372. (October December 1975)","DOI":"10.1007\/BF02575754"}],"container-title":["Lecture Notes in Computer Science","7th International Conference on Automated Deduction"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-0-387-34768-4_12.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,5]],"date-time":"2025-03-05T12:35:45Z","timestamp":1741178145000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-0-387-34768-4_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1984]]},"ISBN":["9780387960227","9780387347684"],"references-count":50,"URL":"https:\/\/doi.org\/10.1007\/978-0-387-34768-4_12","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1984]]}}}