{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T00:42:09Z","timestamp":1725583329618},"publisher-location":"New York, NY","reference-count":27,"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_14","type":"book-chapter","created":{"date-parts":[[2011,5,9]],"date-time":"2011-05-09T04:01:06Z","timestamp":1304913666000},"page":"224-247","source":"Crossref","is-referenced-by-count":7,"title":["A New Equational Unification Method: A Generalisation of Martelli-Montanari\u2019s Algorithm"],"prefix":"10.1007","author":[{"given":"Claude","family":"Kirchner","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"14_CR1","first-page":"279","volume":"296","author":"J. Corbin","year":"1983","unstructured":"CORBIN J. and BIDOIT M. \u201cPour une rehabilitation de l\u2019algorithme d\u2019unification de Robinson\u201d. Note a l\u2019academie de sciences de Paris. T.296, Serie I, p 279. (1983).","journal-title":"Note a l\u2019academie de sciences de Paris"},{"key":"14_CR2","doi-asserted-by":"crossref","unstructured":"DERSHOWITZ N.: \u201cOrderings for term-rewriting systems\u201d. Theorical Computer Science 17\u20133. (1982).","DOI":"10.1016\/0304-3975(82)90026-3"},{"key":"14_CR3","unstructured":"FAGES F.: \u201cFormes canoniques dans les algebres booleennes, et application a la demonstration automatique en logique de premier ordre\u201d. These de 3ieme cycle. Unlversite Paris 6. (1983)."},{"key":"14_CR4","doi-asserted-by":"crossref","unstructured":"FAGES F.: \u201cAssociative-Commutative Unification\u201d Proceedings 7th CADE, Napa Valley, 1984.","DOI":"10.1007\/978-0-387-34768-4_12"},{"key":"14_CR5","unstructured":"FAY M.: \u201cFirst order unification in equational theory\u201d Proc. 4th Workshop on Automata Deduction Texas. (1979)."},{"key":"14_CR6","doi-asserted-by":"crossref","unstructured":"HUET G. and OPPEN D.C.: \u201cEquations and rewrite rules: a survey\u201d in \u201cFormal Languages: Perspectives and open problems\u201d Ed. Book R., Academic Press. (1980).","DOI":"10.1016\/B978-0-12-115350-2.50017-8"},{"key":"14_CR7","unstructured":"HUET G.: \u201cResolution d\u2019equation dans les langages d\u2019ordre 1,2...,\u201d These d\u2019etat, Universite Paris VII. (1976)."},{"key":"14_CR8","doi-asserted-by":"crossref","unstructured":"HULLOT J. M.: \u201cCanonical forms and unification\u201d Proc. 5th Workshop on Automated Deduction Les Arcs. (1980).","DOI":"10.21236\/ADA087640"},{"key":"14_CR9","first-page":"361","volume":"154","author":"J.P. Jouannaud","year":"1983","unstructured":"JOUANNAUD J.P. KIRCHNER C. KIRCHNER H.: \u201cIncremental construction of unification algorithms in equationnal theories\u201d. Proc. of the 10th ICALP. LNCS 154, p 361. (1983).","journal-title":"Incremental construction of unification algorithms in equationnal theories"},{"key":"14_CR10","doi-asserted-by":"crossref","unstructured":"JOUANNAUD J.P. KIRCHNER H.: \u201cCompletion of a set of rules modulo a set of equations\u201d. Proc. of the 11th ACM conference on principles of programming languages, Salt Lake City. (1984).","DOI":"10.1145\/800017.800519"},{"key":"14_CR11","unstructured":"KIRCHNER.: \u2018A new unification method in equational theories and its application to the MINUS theories\u201d. Internal report CRIN 83-R-xxx. (1983)."},{"key":"14_CR12","doi-asserted-by":"crossref","unstructured":"KIRCHNER.: \u201cA general inductive completion algorithm and application to abstract data types\u201d. Proceedings 7th CADE, Napa Valley, 1984.","DOI":"10.1007\/978-0-387-34768-4_17"},{"key":"14_CR13","doi-asserted-by":"crossref","unstructured":"KNUTH D. BENDIX P.: \u201cSimple word problems in universal algebras\u201d in \u201cComputational problems in abstract algebra\u201d Leech J. ed. Pergamon Press, pp 263\u2013297 (1970).","DOI":"10.1016\/B978-0-08-012975-4.50028-X"},{"key":"14_CR14","unstructured":"KIRCHNER C., KIRCHNER H., JOUANNAUD J.P.: \u201cAlgebraic mauipulations as a unification and matching strategy for linear equations in signed binary trees\u201d. Proc. IJCAI 81 Vancouver. (1981)."},{"key":"14_CR15","unstructured":"KIRCHNER C. KIRCHNER H.: \u201cResolution d\u2019equations dans les algebres libres et les varietes eq1ationnelles\u201d. These de 3eme cycle, Universite NANCY 1. (1982)"},{"key":"14_CR16","unstructured":"LANKFORD D.S.: \u201cCanonical inference\u201d. Report ATP-32. University of Texas. (1975)."},{"key":"14_CR17","unstructured":"LANKFORD D.S.: \u201cA unification algorithm for abelian group theory\u201d Report MTP-1. Math. dep., Louisiana Tech. U. (1979)."},{"key":"14_CR18","doi-asserted-by":"crossref","unstructured":"83] LESCANNE P.: \u201cComputer experiments with the REVE term rewriting system generator\u201d. Proc. of the 10th POPL conference. (1983).","DOI":"10.1145\/567067.567078"},{"key":"14_CR19","unstructured":"LIVESEY M. and SIEKMANN J.: \u201cUnification of sets\u201d Report 3\/76, Institut fur Informatik 1, Univ. Karlsruhe. (1977)."},{"issue":"2","key":"14_CR20","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1145\/357162.357169","volume":"4","author":"A. Martelli","year":"1992","unstructured":"MARTELLI A. and MONTANARI U.: \u201cAn efficient unification algorithm\u201d Transactions on Programming Langaages and Systems Vol. 4, Number 2. p 258. (1992).","journal-title":"Transactions on Programming Langaages and Systems"},{"key":"14_CR21","first-page":"73","volume":"7","author":"G. Plotkin","year":"1972","unstructured":"PLOTKIN G.: \u201cBuilding in equational theories\u201d Machine Intelligence 7, pp 73\u201390. (1972).","journal-title":"Machine Intelligence"},{"key":"14_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.: \u201cLinear unification\u201d J. of Computer and Systems Sciences 16 pp 158\u2013167. (1978).","journal-title":"J. of Computer and Systems Sciences"},{"key":"14_CR23","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1145\/321250.321253","volume":"12","author":"J.A. Robinson","year":"1965","unstructured":"ROBINSON J.A.: \u201cA machine oriented logic based on the resolution principle\u201d J.ACM 12, pp 32\u201341. (1965).","journal-title":"J.ACM"},{"key":"14_CR24","unstructured":"ROBINSON J.A.: \u201ccomputational logic: the unification computation\u201d. Machine Intelligence 6. (1971)."},{"key":"14_CR25","unstructured":"RAULEFS P. and SIEKMANN J.: \u201cUnification of idempotent functions\u201d Report, Institut fur Informatik 1, Univ. Karlsruhe. (1978)."},{"key":"14_CR26","first-page":"369","volume":"138","author":"J. Siekmann","year":"1992","unstructured":"SIEKMANN J. and SZABO P.: \u201cUniversal unification and a classification of equational theories\u201d. Proc. of the 6th CADE. LNCS 138, p 369. (1992).","journal-title":"Universal unification and a classification of equational theories"},{"key":"14_CR27","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1145\/322261.322262","volume":"28","author":"M.E. Stickel","year":"1981","unstructured":"STICKEL M.E.: \u201cA unification algorithm for associative-commutative functions\u201d J.ACM 28, no.3, pp 423\u2013434. (1981).","journal-title":"J.ACM"}],"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_14.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:45:15Z","timestamp":1605649515000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-0-387-34768-4_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1984]]},"ISBN":["9780387960227","9780387347684"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-0-387-34768-4_14","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1984]]}}}