{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,19]],"date-time":"2026-03-19T16:52:23Z","timestamp":1773939143589,"version":"3.50.1"},"reference-count":89,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[1979,5,1]],"date-time":"1979-05-01T00:00:00Z","timestamp":294364800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["SIGSAM Bull."],"published-print":{"date-parts":[[1979,5]]},"abstract":"<jats:p>\n            1. Motivations There is a wide variety of areas where matching and unification problems arise: (1.1)\n            <jats:italic>Databases<\/jats:italic>\n            The user of a\n            <jats:italic>(relational) database<\/jats:italic>\n            [22] may logically AND the properties she wants to retrieve or else she may be interested in the NATURAL JOIN [17] of two stored relations. In neither case, she would appreciate if she constantly had to take into account that AND is an associative and commutative operation, or that NATURAL JOIN obeys an associative axiom, which may distribute over some other operation [68].\n          <\/jats:p>","DOI":"10.1145\/1089208.1089210","type":"journal-article","created":{"date-parts":[[2007,1,17]],"date-time":"2007-01-17T18:32:02Z","timestamp":1169058722000},"page":"14-20","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":25,"title":["A short survey on the state of the art in matching and unification problems"],"prefix":"10.1145","volume":"13","author":[{"given":"P.","family":"Raulefs","sequence":"first","affiliation":[{"name":"Universit\u00e4t Bonn, Kurf\u00fcrstenstr, Bonn"}]},{"given":"J.","family":"Siekmann","sequence":"additional","affiliation":[{"name":"Universit\u00e4t Karlsruhe, Postfach, Karlsruhe"}]},{"given":"P.","family":"Szab\u00f3","sequence":"additional","affiliation":[{"name":"Universit\u00e4t Karlsruhe, Postfach, Karlsruhe"}]},{"given":"E.","family":"Unvericht","sequence":"additional","affiliation":[{"name":"Universit\u00e4t Karlsruhe, Postfach, Karlsruhe"}]}],"member":"320","published-online":{"date-parts":[[1979,5]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"ATP-39","author":"Ballantyne D.","year":"1977","unstructured":"A. Ballantyne , D. Lankford; ' Decision Procedures for simple equational theories', University of Texas at Austin, ATP-35, ATP-37 , ATP-39 , 1977 A. Ballantyne, D. Lankford; 'Decision Procedures for simple equational theories', University of Texas at Austin, ATP-35, ATP-37, ATP-39, 1977"},{"key":"e_1_2_1_2_1","volume-title":"Frontiers of Pattern Recognition","author":"Barrow Ambler","year":"1972","unstructured":"Barrow , Ambler , Burstall; 'Some techniques for recognizing Structures in Pictures' , Frontiers of Pattern Recognition , Academic Press Inc ., 1972 Barrow, Ambler, Burstall; 'Some techniques for recognizing Structures in Pictures', Frontiers of Pattern Recognition, Academic Press Inc., 1972"},{"key":"e_1_2_1_3_1","volume-title":"Dept. of Analysis and Computer Science","author":"Unification Algorithm' Rep","year":"1973","unstructured":"L.D. Baxter; 'An efficient Unification Algorithm' , Rep . CS-73-23 , University of Waterloo , Dept. of Analysis and Computer Science , 1973 L.D. Baxter; 'An efficient Unification Algorithm', Rep. CS-73-23, University of Waterloo, Dept. of Analysis and Computer Science, 1973"},{"key":"e_1_2_1_4_1","volume-title":"Applied Logic Corp","author":"Bennett Easton","year":"1963","unstructured":"Bennett , Easton , Guard , Settle; 'CRT-aided semiautomated mathematics', AFCRL-63 , Applied Logic Corp ., 1963 Bennett, Easton, Guard, Settle; 'CRT-aided semiautomated mathematics', AFCRL-63, Applied Logic Corp., 1963"},{"key":"e_1_2_1_5_1","volume-title":"Applied Logic Corporation","author":"Bennett","year":"1965","unstructured":"Bennett , Easton; 'CRT-aided semi-automated mathematics', AFCRL-65 , Applied Logic Corporation , 1965 Bennett, Easton; 'CRT-aided semi-automated mathematics', AFCRL-65, Applied Logic Corporation, 1965"},{"key":"e_1_2_1_6_1","unstructured":"Bennett Easton Guard Settle; 'CRT-aided semi-automated mathematics' AFCRL-67-0167. Applied Corp. Princeton  Bennett Easton Guard Settle; 'CRT-aided semi-automated mathematics' AFCRL-67-0167. Applied Corp. Princeton"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/800204.806266"},{"key":"e_1_2_1_8_1","volume-title":"Proc. of IFIP, North Holland Publishing Comp.","author":"Symbol Manipulation Languages'","year":"1968","unstructured":"D. G. Bobrow (ed.); ' Symbol Manipulation Languages' , Proc. of IFIP, North Holland Publishing Comp. , 1968 D. G. Bobrow (ed.); 'Symbol Manipulation Languages', Proc. of IFIP, North Holland Publishing Comp., 1968"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/800228.806938"},{"issue":"1","key":"e_1_2_1_10_1","article-title":"A New Representation Language","volume":"9","author":"Directed Recursive Labelnode Hypergraphs","year":"1977","unstructured":"H. Boley; ' Directed Recursive Labelnode Hypergraphs : A New Representation Language ', Journal of Artificial Intelligence , vol 9 , no. 1 , 1977 H. Boley; 'Directed Recursive Labelnode Hypergraphs: A New Representation Language', Journal of Artificial Intelligence, vol 9, no. 1, 1977","journal-title":"Journal of Artificial Intelligence"},{"key":"e_1_2_1_11_1","first-page":"2","article-title":"methods used with transistor patent applications","volume":"3","author":"Bryan J.","year":"1966","unstructured":"H. Bryan , J. Carnog; ' Search methods used with transistor patent applications ', IEEE Spectrum 3 , 2 , 1966 H. Bryan, J. Carnog; 'Search methods used with transistor patent applications', IEEE Spectrum 3, 2, 1966","journal-title":"IEEE Spectrum"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/321574.321591"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/800204.806276"},{"key":"e_1_2_1_14_1","author":"On Seeing Things'","year":"1971","unstructured":"M. Clowes; ' On Seeing Things' , Journal of Artificial Intelligence , 1971 M. Clowes; 'On Seeing Things', Journal of Artificial Intelligence, 1971","journal-title":"Journal of Artificial Intelligence"},{"key":"e_1_2_1_15_1","unstructured":"CODASYL Systems Committee; 'A survey of Generalized Data Base Management Systems' Techn. Rep. 1969 ACM and IAG  CODASYL Systems Committee; 'A survey of Generalized Data Base Management Systems' Techn. Rep. 1969 ACM and IAG"},{"key":"e_1_2_1_16_1","doi-asserted-by":"crossref","unstructured":"CODASYL Systems Committee; 'Feature Analysis of Generalized Data Base Management Systems' TR 1971 ACM BC and IAG  CODASYL Systems Committee; 'Feature Analysis of Generalized Data Base Management Systems' TR 1971 ACM BC and IAG","DOI":"10.1145\/362588.362590"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/362384.362685"},{"key":"e_1_2_1_18_1","volume-title":"in Data Base Systems","author":"Data Base Sublanguages'","year":"1972","unstructured":"E. F. Codd; 'Relational Completeness of Data Base Sublanguages' , in Data Base Systems , Prentice Hall , Courant Comp . Science Symposia Series, vol 6, 1972 E. F. Codd; 'Relational Completeness of Data Base Sublanguages', in Data Base Systems, Prentice Hall, Courant Comp. Science Symposia Series, vol 6, 1972"},{"key":"e_1_2_1_19_1","volume-title":"Cal.","author":"Algebraic","year":"1965","unstructured":"Cook; ' Algebraic techniques and the mechanization of number theory', RM-4319-PR, Rand Corp., Santa Monica , Cal. , 1965 Cook; 'Algebraic techniques and the mechanization of number theory', RM-4319-PR, Rand Corp., Santa Monica, Cal., 1965"},{"key":"e_1_2_1_20_1","volume-title":"of Computer Science","author":"Graph Isomorphism' Ph. D.","year":"1968","unstructured":"D. G. Corneil; ' Graph Isomorphism' , Ph. D. Dept . of Computer Science , University of Toronto , 1968 D. G. Corneil; 'Graph Isomorphism', Ph. D. Dept. of Computer Science, University of Toronto, 1968"},{"key":"e_1_2_1_21_1","unstructured":"J. L. Darlington; 'A partial Mechanization of Second Order Logic' Mach. Int. 6 1971  J. L. Darlington; 'A partial Mechanization of Second Order Logic' Mach. Int. 6 1971"},{"key":"e_1_2_1_22_1","volume-title":"Comp","author":"Database Systems' Addison-Wesley","year":"1976","unstructured":"C. J. Date; 'An Introduction to Database Systems' , Addison-Wesley Publ . Comp . Inc . 1976 C. J. Date; 'An Introduction to Database Systems', Addison-Wesley Publ. Comp. Inc. 1976"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/800204.806300"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/321203.321207"},{"key":"e_1_2_1_25_1","volume-title":"Report 41","author":"Fischer S.","year":"1974","unstructured":"J. Fischer , S. Patterson; ' String Matching and other Products', MIT, Project MAC , Report 41 , 1974 J. Fischer, S. Patterson; 'String Matching and other Products', MIT, Project MAC, Report 41, 1974"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/361952.361960"},{"key":"e_1_2_1_27_1","volume-title":"Scientific report No. 4","year":"1966","unstructured":"W. E. Gould; 'A matching procedure for \u03c9-order logic' , Scientific report No. 4 , Air Force Cambridge Research Labs ., 1966 W. E. Gould; 'A matching procedure for \u03c9-order logic', Scientific report No. 4, Air Force Cambridge Research Labs., 1966"},{"key":"e_1_2_1_28_1","first-page":"710","article-title":"logic for semi automated mathematics', Scientific report No. 1, Air Force Cambridge Research Labs","volume":"602","author":"Automated","year":"1964","unstructured":"J. R. Guard; ' Automated logic for semi automated mathematics', Scientific report No. 1, Air Force Cambridge Research Labs ., AD 602 710 , 1964 J. R. Guard; 'Automated logic for semi automated mathematics', Scientific report No. 1, Air Force Cambridge Research Labs., AD 602 710, 1964","journal-title":"AD"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/800204.806277"},{"key":"e_1_2_1_30_1","unstructured":"S. Heilbrunner; 'Gleichungssysteme f\u00fcr Zeichenreihen' TU M\u00fcnchen Abtl. Mathematik Ber. Nr. 7311 1973  S. Heilbrunner; 'Gleichungssysteme f\u00fcr Zeichenreihen' TU M\u00fcnchen Abtl. Mathematik Ber. Nr. 7311 1973"},{"key":"e_1_2_1_32_1","volume-title":"Working paper 92","author":"Passing Massages' MIT","year":"1976","unstructured":"C. Hewitt; 'Viewing Control Structures as Patterns of Passing Massages' , MIT , AI- Lab . , Working paper 92 , 1976 C. Hewitt; 'Viewing Control Structures as Patterns of Passing Massages', MIT, AI-Lab., Working paper 92, 1976"},{"key":"e_1_2_1_33_1","first-page":"5","article-title":"solution of certain systems of word equations","volume":"749","author":"The","year":"1964","unstructured":"J. I. Hmelevskij; ' The solution of certain systems of word equations ', Dokl. Akad. Nauk SSSR , 1964 , 749 Soviet Math. Dokl. 5 , 1964, 724 J. I. Hmelevskij; 'The solution of certain systems of word equations', Dokl. Akad. Nauk SSSR, 1964, 749 Soviet Math. Dokl. 5, 1964, 724","journal-title":"Dokl. Akad. Nauk SSSR"},{"key":"e_1_2_1_34_1","unstructured":"J. I. Hmelevskij; 'Word equations without coefficients' Dokl. Akad. Nauk. SSSR 171 1966 1047 Soviet Math. Dokl.7 1966 1611  J. I. Hmelevskij; 'Word equations without coefficients' Dokl. Akad. Nauk. SSSR 171 1966 1047 Soviet Math. Dokl.7 1966 1611"},{"key":"e_1_2_1_35_1","unstructured":"J. I. Hmelevskij; 'Solution of word equations in three unknowns' Dokl. Akad. Nauk. SSSR 177 1967 No. 5 Soviet Math. Dokl. 8 1967 No. 6  J. I. Hmelevskij; 'Solution of word equations in three unknowns' Dokl. Akad. Nauk. SSSR 177 1967 No. 5 Soviet Math. Dokl. 8 1967 No. 6"},{"key":"e_1_2_1_36_1","volume-title":"a complete method for theory","year":"1972","unstructured":"G. P. Huet; 'Constrained resolution : a complete method for theory ', Jenning's Computing Centre rep. 1117, Case Western Reserve Univ. , 1972 G. P. Huet; 'Constrained resolution: a complete method for theory', Jenning's Computing Centre rep. 1117, Case Western Reserve Univ., 1972"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(73)90301-X"},{"key":"e_1_2_1_38_1","volume-title":"\u03bb-Calculus and Comp. Sci. Theory","author":"Lambda Calculus'","year":"1975","unstructured":"G. Huet; 'Unification in typed Lambda Calculus' , in: \u03bb-Calculus and Comp. Sci. Theory , Springer Lecture Notes , No . 37, Proc. of the Symp. held in Rome, 1975 G. Huet; 'Unification in typed Lambda Calculus', in: \u03bb-Calculus and Comp. Sci. Theory, Springer Lecture Notes, No. 37, Proc. of the Symp. held in Rome, 1975"},{"key":"e_1_2_1_39_1","article-title":"Algorithm for typed \u03bb-Calculus","volume":"1","author":"Unification","year":"1975","unstructured":"G. P. Huet; 'A Unification Algorithm for typed \u03bb-Calculus ', J. Theor. Comp. Sci. , 1 , 1975 G. P. Huet; 'A Unification Algorithm for typed \u03bb-Calculus', J. Theor. Comp. Sci., 1, 1975","journal-title":"J. Theor. Comp. Sci."},{"key":"e_1_2_1_40_1","volume-title":"w","year":"1976","unstructured":"G. Huet; 'R\u00e9solution d'\u00e9quations dans des langages d'ordre 1.2,.. , w ; Th\u00e8se d'etat, IRIA-Laboria , 1976 G. Huet; 'R\u00e9solution d'\u00e9quations dans des langages d'ordre 1.2,.., w; Th\u00e8se d'etat, IRIA-Laboria, 1976"},{"key":"e_1_2_1_41_1","volume-title":"Rocquencourt","author":"Confluent Reductions","year":"1977","unstructured":"G. Huet; ' Confluent Reductions : Abstract Properties and Applications to Term Rewriting Systems', IRIA-Laboria, Rap. de Recherche no. 250 , Rocquencourt , 1977 G. Huet; 'Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems', IRIA-Laboria, Rap. de Recherche no. 250, Rocquencourt, 1977"},{"key":"e_1_2_1_42_1","volume-title":"of Applied Analysis and Comp. Sci","author":"Jensen T.","year":"1973","unstructured":"D. Jensen , T. Pietrzykowski; 'Mechanising \u03c9-order type theory through unification', Rep . CS-73-16, Dept . of Applied Analysis and Comp. Sci . University of Waterloo , 1973 D. Jensen, T. Pietrzykowski; 'Mechanising \u03c9-order type theory through unification', Rep. CS-73-16, Dept. of Applied Analysis and Comp. Sci. University of Waterloo, 1973"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/800152.804905"},{"key":"e_1_2_1_44_1","volume-title":"in Computational Problems in Abstract Algebra","author":"Knuth P. B.","year":"1970","unstructured":"D. E. Knuth , P. B. Bendix; ' Simple Word Problems in Universal Algebras' , in Computational Problems in Abstract Algebra , J. Leech (ed.), Pergamon Press , Oxford , 1970 D. E. Knuth, P. B. Bendix; 'Simple Word Problems in Universal Algebras', in Computational Problems in Abstract Algebra, J. Leech (ed.), Pergamon Press, Oxford, 1970"},{"key":"e_1_2_1_45_1","volume-title":"Comp. Sci. Dept.","author":"Knuth Morris","year":"1974","unstructured":"Knuth , Morris , Pratt; ' Fast Pattern Matching in Strings' , Stan-CS-74-440 , Stanford University , Comp. Sci. Dept. , 1974 Knuth, Morris, Pratt; 'Fast Pattern Matching in Strings', Stan-CS-74-440, Stanford University, Comp. Sci. Dept., 1974"},{"key":"e_1_2_1_46_1","volume-title":"Proceedings of fourth IJCAI-77","author":"K\u00fchner Ch.","unstructured":"S. K\u00fchner , Ch. Mathis , P. Raulefs , J. Siekmann; 'Unification of Idempotent Functions' , Proceedings of fourth IJCAI-77 , MIT , Cambridge S. K\u00fchner, Ch. Mathis, P. Raulefs, J. Siekmann; 'Unification of Idempotent Functions', Proceedings of fourth IJCAI-77, MIT, Cambridge"},{"key":"e_1_2_1_47_1","volume-title":"Nota Interna B73-12","author":"Levi F.","year":"1973","unstructured":"G. Levi , F. Sirovich; ' Pattern Matching and Goal directed Computation' , Nota Interna B73-12 , Univ. of Pisa , 1973 G. Levi, F. Sirovich; 'Pattern Matching and Goal directed Computation', Nota Interna B73-12, Univ. of Pisa, 1973"},{"key":"e_1_2_1_48_1","volume-title":"Essex University","author":"Livesey J.","year":"1975","unstructured":"M. Livesey , J. Siekmann; ' Termination and Decidability Results for String Unification' , Essex University , Computer Centre Memo CSM- 12, 1975 M. Livesey, J. Siekmann; 'Termination and Decidability Results for String Unification', Essex University, Computer Centre Memo CSM-12, 1975"},{"key":"e_1_2_1_49_1","volume-title":"f. Informatik I","author":"Livesey J.","unstructured":"M. Livesey , J. Siekmann; 'Unification of Sets' , Int . Ber . 3\/76, Inst . f. Informatik I , Univ. Karlsruhe M. Livesey, J. Siekmann; 'Unification of Sets', Int. Ber. 3\/76, Inst. f. Informatik I, Univ. Karlsruhe"},{"key":"e_1_2_1_50_1","volume-title":"Rep. CSRR 2059","author":"The","year":"1972","unstructured":"C. L. Lucchesi; ' The undecidability of the unification problem for third order languages ', Rep. CSRR 2059 , Dept. of Applied Analysis and Comp. Science, University of Waterloo , 1972 C. L. Lucchesi; 'The undecidability of the unification problem for third order languages', Rep. CSRR 2059, Dept. of Applied Analysis and Comp. Science, University of Waterloo, 1972"},{"key":"e_1_2_1_51_1","volume-title":"no. 2","author":"Free Semigroup' Soviet","year":"1977","unstructured":"G. S. Makanin; 'The Problem of Solvability of Equations in a Free Semigroup' , Soviet . Akad . Nauk SSSR, TOM 233 , no. 2 , 1977 G. S. Makanin; 'The Problem of Solvability of Equations in a Free Semigroup', Soviet. Akad. Nauk SSSR, TOM 233, no. 2, 1977"},{"key":"e_1_2_1_52_1","volume-title":"IFIP Conf. on Symb. Manip.","author":"Manove Bloom","year":"1968","unstructured":"Manove , Bloom , Engelmann; ' Rational Functions in MATHLA B' , IFIP Conf. on Symb. Manip. , Pisa , 1968 Manove, Bloom, Engelmann; 'Rational Functions in MATHLAB', IFIP Conf. on Symb. Manip., Pisa, 1968"},{"key":"e_1_2_1_53_1","first-page":"1038","article-title":"Steklov', No. 42, Izdat. Akad. Nauk SSSR, 1954","volume":"17","author":"Trudy Mat Inst","year":"1954","unstructured":"A. A. Markov; ' Trudy Mat . Inst . Steklov', No. 42, Izdat. Akad. Nauk SSSR, 1954 , MR 17 , 1038 , 1954 A. A. Markov; 'Trudy Mat. Inst. Steklov', No. 42, Izdat. Akad. Nauk SSSR, 1954, MR 17, 1038, 1954","journal-title":"MR"},{"key":"e_1_2_1_54_1","volume-title":"Report","author":"Strings' Universit\u00e4t Karlsruhe","year":"1977","unstructured":"Maurer; 'Graphs as Strings' , Universit\u00e4t Karlsruhe , Techn . Report , 1977 Maurer; 'Graphs as Strings', Universit\u00e4t Karlsruhe, Techn. Report, 1977"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/362637.362651"},{"key":"e_1_2_1_56_1","doi-asserted-by":"crossref","unstructured":"J. Moses; 'MACSYMA - the fifth Year' Project MAC MIT Cambridge 1974  J. Moses; 'MACSYMA - the fifth Year' Project MAC MIT Cambridge 1974","DOI":"10.1145\/1086837.1086857"},{"key":"e_1_2_1_57_1","volume-title":"Techn. Rep.","year":"1971","unstructured":"A. Nevins; 'A human-oriented logic for automatic theorem proving', George Washington University , Techn. Rep. , 1971 A. Nevins; 'A human-oriented logic for automatic theorem proving', George Washington University, Techn. Rep., 1971"},{"key":"e_1_2_1_59_1","volume-title":"Techn. Rep.","author":"Peterson M. E.","year":"1978","unstructured":"G. E. Peterson , M. E. Stickel; ' Complete Sets of Reductions for Equational Theories with Complete Unification Algorithms' , University of Arizona , Techn. Rep. , 1978 G. E. Peterson, M. E. Stickel; 'Complete Sets of Reductions for Equational Theories with Complete Unification Algorithms', University of Arizona, Techn. Rep., 1978"},{"key":"e_1_2_1_60_1","volume-title":"vol 7","author":"Mach Intelligence","year":"1972","unstructured":"G. Plotkin; 'Building in equational theories', Mach . Intelligence , vol 7 , 1972 G. Plotkin; 'Building in equational theories', Mach. Intelligence, vol 7, 1972"},{"key":"e_1_2_1_61_1","volume-title":"MIP-R-62","author":"Matching' Univ","year":"1969","unstructured":"J. Rastall; 'Graph-family Matching' , Univ . of Edinburgh , MIP-R-62 , 1969 J. Rastall; 'Graph-family Matching', Univ. of Edinburgh, MIP-R-62, 1969"},{"key":"e_1_2_1_62_1","unstructured":"P. Raulefs J. Siekmann; 'Unification of Idempotent Functions' (extended and revised version of {46} 1978  P. Raulefs J. Siekmann; 'Unification of Idempotent Functions' (extended and revised version of {46} 1978"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/321250.321253"},{"key":"e_1_2_1_64_1","volume-title":"Symp. Appl. Math., vol 19","year":"1967","unstructured":"J. A. Robinson; 'A review on automatic theorem proving ', Symp. Appl. Math., vol 19 , 1--18, 1967 J. A. Robinson; 'A review on automatic theorem proving', Symp. Appl. Math., vol 19, 1--18, 1967"},{"key":"e_1_2_1_65_1","volume-title":"Mach. Intell. 6","author":"Computational Logic","year":"1970","unstructured":"J. A. Robinson; ' Computational Logic : The Unification Computation ', Mach. Intell. 6 , 1970 J. A. Robinson; 'Computational Logic: The Unification Computation', Mach. Intell. 6, 1970"},{"key":"e_1_2_1_66_1","volume-title":"North Holland","author":"Robinson L.","year":"1973","unstructured":"G. Robinson , L. Wos; ' Maximal models and refutation completeness: Semidecision procedures in automatic theorem proving', in Boone et al. (eds.), \"Word problems \", North Holland , 1973 G. Robinson, L. Wos; 'Maximal models and refutation completeness: Semidecision procedures in automatic theorem proving', in Boone et al. (eds.), \"Word problems\", North Holland, 1973"},{"key":"e_1_2_1_67_1","volume-title":"Stanford Univ.","author":"Rulifson Derksen","year":"1972","unstructured":"Rulifson , Derksen , Waldinger; 'QA4 : A procedural calculus for intuitive reasoning ', Stanford Univ. , Nov. 1972 Rulifson, Derksen, Waldinger; 'QA4: A procedural calculus for intuitive reasoning', Stanford Univ., Nov. 1972"},{"key":"e_1_2_1_68_1","unstructured":"This interesting area of application was pointed out to us by W. Sch\u00f6nfeld Universit\u00e4t Stuttgart  This interesting area of application was pointed out to us by W. Sch\u00f6nfeld Universit\u00e4t Stuttgart"},{"key":"e_1_2_1_69_1","unstructured":"J. Siekmann; 'Stringunification' Essex University Memo CSM-7 1975  J. Siekmann; 'Stringunification' Essex University Memo CSM-7 1975"},{"key":"e_1_2_1_70_1","unstructured":"J. Siekmann; 'Unification of commutative terms' Universit\u00e4t Karlsruhe. Int. Bericht 2 1976  J. Siekmann; 'Unification of commutative terms' Universit\u00e4t Karlsruhe. Int. Bericht 2 1976"},{"key":"e_1_2_1_71_1","unstructured":"J. Siekmann; 'Unification and Matching Problems' Ph.D. Essex University MEMO CSM-4-78  J. Siekmann; 'Unification and Matching Problems' Ph.D. Essex University MEMO CSM-4-78"},{"key":"e_1_2_1_72_1","volume-title":"vol 11, no. 3","author":"Algebraic Manipulation'","year":"1977","unstructured":"SIGSAM Bulletin; 'ACM special interest group on Symbolic and Algebraic Manipulation' , vol 11, no. 3 , 1977 (issue no. 43) contains an almost complete bibliography SIGSAM Bulletin; 'ACM special interest group on Symbolic and Algebraic Manipulation', vol 11, no. 3, 1977 (issue no. 43) contains an almost complete bibliography"},{"key":"e_1_2_1_73_1","first-page":"289","volume":"7","author":"Skordew B.","year":"1961","unstructured":"D. Skordew , B. Sendow; ' Z. Math. Logic Grundlagen' , Math. 7 ( 1961 ), 289 , MR 31, 57 (russian) (English translation at University of Essex, Comp. Sci. Dept.) D. Skordew, B. Sendow; 'Z. Math. Logic Grundlagen', Math. 7 (1961), 289, MR 31, 57 (russian) (English translation at University of Essex, Comp. Sci. Dept.)","journal-title":"Math."},{"key":"e_1_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.1145\/321679.321689"},{"key":"e_1_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.1145\/321850.321859"},{"key":"e_1_2_1_76_1","unstructured":"B. C. Smith C. Hewitt; 'A Plasma Primer' MIT AI-Lab. 1975  B. C. Smith C. Hewitt; 'A Plasma Primer' MIT AI-Lab. 1975"},{"key":"e_1_2_1_77_1","volume-title":"CSRG-39","author":"String Patterns'","year":"1974","unstructured":"G. F. Stewart; 'An Algebraic Model for String Patterns' , University of Toronto , CSRG-39 , 1974 G. F. Stewart; 'An Algebraic Model for String Patterns', University of Toronto, CSRG-39, 1974"},{"key":"e_1_2_1_78_1","volume-title":"Proc. 4th IJCAI, Tbilis, USSR","year":"1975","unstructured":"M. E. Stickel; 'A complete unification algorithm for associative, commutative Functions ', Proc. 4th IJCAI, Tbilis, USSR , 1975 M. E. Stickel; 'A complete unification algorithm for associative, commutative Functions', Proc. 4th IJCAI, Tbilis, USSR, 1975"},{"key":"e_1_2_1_79_1","first-page":"1","article-title":"graph-theoretical algorithm for matching chemical structures","volume":"5","year":"1965","unstructured":"E. Sussenguth; 'A graph-theoretical algorithm for matching chemical structures ', J. Chem. Doc. 5 , 1 , 1965 E. Sussenguth; 'A graph-theoretical algorithm for matching chemical structures', J. Chem. Doc. 5, 1, 1965","journal-title":"J. Chem. Doc."},{"key":"e_1_2_1_80_1","unstructured":"P. Szab\u00f3; 'The Undecidability of the DA-Unification Problem; Universit\u00e4t Karlsruhe Int. Ber. 3 1978  P. Szab\u00f3; 'The Undecidability of the DA-Unification Problem; Universit\u00e4t Karlsruhe Int. Ber. 3 1978"},{"key":"e_1_2_1_81_1","unstructured":"P. Szab\u00f3 E. Unvericht; 'D-Unification has infinitely many mgus' Universit\u00e4t Karlsruhe Inst. f. Informatik I (forthcoming)  P. Szab\u00f3 E. Unvericht; 'D-Unification has infinitely many mgus' Universit\u00e4t Karlsruhe Inst. f. Informatik I (forthcoming)"},{"key":"e_1_2_1_82_1","doi-asserted-by":"publisher","DOI":"10.1145\/321921.321925"},{"key":"e_1_2_1_83_1","doi-asserted-by":"publisher","DOI":"10.1145\/363872.363899"},{"key":"e_1_2_1_84_1","volume-title":"Proc. of Fourth IJCAI, Tbilisi, USSR","year":"1975","unstructured":"J. van Vaalen; 'An Extension of Unification to Substitutions with an Application to ATP ', Proc. of Fourth IJCAI, Tbilisi, USSR , 1975 J. van Vaalen; 'An Extension of Unification to Substitutions with an Application to ATP', Proc. of Fourth IJCAI, Tbilisi, USSR, 1975"},{"key":"e_1_2_1_85_1","volume-title":"forthcoming","author":"Unifikation von Morphismen' Diplomarbeit","year":"1978","unstructured":"E. Vogel; ' Unifikation von Morphismen' , Diplomarbeit , forthcoming , 1978 E. Vogel; 'Unifikation von Morphismen', Diplomarbeit, forthcoming, 1978"},{"key":"e_1_2_1_86_1","volume-title":"D.A.I. Research Rep. no. 39","author":"G'","year":"1977","unstructured":"D. H. D. Warren; 'Implementing PROLO G' , vol 1 and vol 2 , D.A.I. Research Rep. no. 39 , University of Edinburgh , 1977 D. H. D. Warren; 'Implementing PROLOG', vol 1 and vol 2, D.A.I. Research Rep. no. 39, University of Edinburgh, 1977"},{"key":"e_1_2_1_87_1","volume-title":"IEEE Symp. on Sw. and Automata Theory, 14","author":"Linear Pattern Matching Algorithms'","year":"1973","unstructured":"P. Weiner; ' Linear Pattern Matching Algorithms' , IEEE Symp. on Sw. and Automata Theory, 14 , 1973 P. Weiner; 'Linear Pattern Matching Algorithms', IEEE Symp. on Sw. and Automata Theory, 14, 1973"},{"key":"e_1_2_1_88_1","volume-title":"on the Algorithmic Language ALGOL68","author":"Revised Rep","year":"1976","unstructured":"van Wijngaarden ( Revised Rep . on the Algorithmic Language ALGOL68 ', Springer-Verlag, Berlin, Heidelberg , N.Y. , 1976 van Wijngaarden (et al); 'Revised Rep. on the Algorithmic Language ALGOL68', Springer-Verlag, Berlin, Heidelberg, N.Y., 1976"},{"key":"e_1_2_1_89_1","unstructured":"Winston; 'The Psychology of Computer Vision' 1975 McGraw Hill  Winston; 'The Psychology of Computer Vision' 1975 McGraw Hill"},{"key":"e_1_2_1_90_1","unstructured":"G. Winterstein; 'Unification in Second Order Logic' Bericht 3 Univ. Kaiserslautern 1976  G. Winterstein; 'Unification in Second Order Logic' Bericht 3 Univ. Kaiserslautern 1976"},{"key":"e_1_2_1_91_1","doi-asserted-by":"publisher","DOI":"10.1145\/321921.321923"}],"container-title":["ACM SIGSAM Bulletin"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1089208.1089210","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1089208.1089210","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T16:08:22Z","timestamp":1750262902000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1089208.1089210"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1979,5]]},"references-count":89,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1979,5]]}},"alternative-id":["10.1145\/1089208.1089210"],"URL":"https:\/\/doi.org\/10.1145\/1089208.1089210","relation":{},"ISSN":["0163-5824"],"issn-type":[{"value":"0163-5824","type":"print"}],"subject":[],"published":{"date-parts":[[1979,5]]},"assertion":[{"value":"1979-05-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}