{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T14:03:56Z","timestamp":1725631436238},"publisher-location":"Berlin, Heidelberg","reference-count":128,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540119609"},{"type":"electronic","value":"9783642688263"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1982]]},"DOI":"10.1007\/978-3-642-68826-3_9","type":"book-chapter","created":{"date-parts":[[2011,11,8]],"date-time":"2011-11-08T13:53:02Z","timestamp":1320760382000},"page":"102-141","source":"Crossref","is-referenced-by-count":8,"title":["Universal Unification"],"prefix":"10.1007","author":[{"given":"J.","family":"Siekmann","sequence":"first","affiliation":[]},{"given":"P.","family":"Szab\u00f3","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"9_CR1","volume-title":"Decision Procedures for simple equational theories","author":"A Ballantyne","year":"1977","unstructured":"A. Ballantyne, D. Lankford:\u2018Decision Procedures for simple equational theories\u2019, University of Texas at Austin, ATP-35, ATP-37, ATP-39, 1977"},{"key":"9_CR2","volume-title":"Frontiers of Pattern Recognition","author":"Barrow","year":"1972","unstructured":"Barrow, Ambler, Burstall: \u2018Some techniques for recognizing Structures in Pictures\u2019, Frontiers of Pattern Recognition, Academic Press Inc., 1972"},{"key":"9_CR3","volume-title":"An efficient Unification Algorithm, Rep. CS-73\u201323","author":"LD Baxter","year":"1973","unstructured":"L.D. Baxter: \u2018An efficient Unification Algorithm\u2019, Rep. CS-73\u201323, University of Waterloo, Dept. of Analysis and Computer Science, 1973"},{"key":"9_CR4","volume-title":"Proc. of the 2nd Symposium on Symbolic Manipulation","author":"F Blair","year":"1971","unstructured":"F. Blair et al: \u2018SCRATCHPAD\/1: An interactive facility for symbolic mathematics\u2019, Proc. of the 2nd Symposium on Symbolic Manipulation, Los Angeles, 1971"},{"volume-title":"Symbol Manipulation Languages","year":"1968","key":"9_CR5","unstructured":"D.G. Bobrow (ed): \u2018Symbol Manipulation Languages\u2019, Proc. of IFIP, North Holland Publishing Comp., 1968"},{"key":"9_CR6","volume-title":"Proc. of ACM","author":"HP B\u00f6hm","year":"1977","unstructured":"H.P. B\u00f6hm, H.L. Fischer, P. Raulefs: \u2018CSSA: Language Concepts and Programming Methodology\u2019, Proc. of ACM, SIGPLAN\/ART Conference, Rochester, 1977"},{"key":"9_CR7","volume-title":"Journal of Artificial Intelligence","author":"H Boley","year":"1977","unstructured":"H. Boley: \u2018Directed Recursive Labelnode Hypergraphs: A New Representation Language\u2019, Journal of Artificial Intelligence, vol 9, no. 1, 1977"},{"key":"9_CR8","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1109\/MSPEC.1966.5216608","volume":"3","author":"H Bryan","year":"1966","unstructured":"H. Bryan, J. Carnog: \u2018Search methods used with transistor patent applications\u2019, IEEE Spectrum 3, 2, 1966","journal-title":"IEEE Spectrum"},{"key":"9_CR9","volume-title":"Information and Control","author":"LD Baxter","year":"1978","unstructured":"L.D. Baxter: \u2018The Undecidability of the Third Order Dyadic Unification Problem\u2019,Information and Control, vol 38, no. 2, 1978"},{"key":"9_CR10","volume-title":"CACM","author":"R Boyer","year":"1977","unstructured":"R. Boyer, J.S. Moore: \u2018A Fast String Searching Algorithm\u2019, CACM vol 20, no. 10, 1977"},{"key":"9_CR11","volume-title":"JACM","author":"Caviness","year":"1970","unstructured":"Caviness: \u2018On Canonical Form and Simplification\u2019, JACM, vol 17, no. 2, 1970"},{"key":"9_CR12","volume-title":"Proc. of the 2nd Symposium on Symbolic Manipulation","author":"C Christensen","year":"1971","unstructured":"C. Christensen, M. Karr: \u2018IAM, a Symstem for interactive algebraic Manipulation\u2019, Proc. of the 2nd Symposium on Symbolic Manipulation, Los Angeles, 1971"},{"key":"9_CR13","volume-title":"Journal of Artificial Intelligence","author":"M Clowes","year":"1971","unstructured":"M. Clowes: \u2018On Seeing Things\u2019 Journal of Artificial Intelligence, 1971"},{"key":"9_CR14","volume-title":"Techn. Rep","author":"CODASYL Systems","year":"1969","unstructured":"CODASYL Systems Committee: \u2018A survey of Generalized Data Base Management Systems\u2019, Techn. Rep. 1969, ACM and IAG"},{"key":"9_CR15","volume-title":"Committee: Feature Analysis of Generalized Data Base Management Systems","author":"CODASYL Systems","year":"1971","unstructured":"CODASYL Systems Committee: \u2018Feature Analysis of Generalized Data Base Management Systems\u2019, TR 1971, ACM, BC and IAG"},{"key":"9_CR16","first-page":"6","volume":"13","author":"EF Codd","year":"1970","unstructured":"E.F. Codd: \u2018A Relational Model of Data for Large shared Data-banks\u2019, CACM, 13, 6, 1970","journal-title":"CACM"},{"key":"9_CR17","volume-title":"Data Base Systems, Prentice Hall, Courant Comp. Science Symposia Series","author":"EF Codd","year":"1972","unstructured":"E.F. Codd: \u2018Relational Completeness of Data Base Sublanguages\u2019, in Data Base Systems, Prentice Hall, Courant Comp. Science Symposia Series, vol 6, 1972"},{"key":"9_CR18","volume-title":"Algebraic techniques and the mechanization of number theory","author":"Cook","year":"1965","unstructured":"Cook: \u2018Algebraic techniques and the mechanization of number theory\u2019, RM-4319-PR, Rand Corp., Santa Monica, Cal., 1965"},{"key":"9_CR19","volume-title":"Graph Isomorphism","author":"DG Corneil","year":"1968","unstructured":"D.G. Corneil: \u2018Graph Isomorphism\u2019, Ph. D. Dept. of Computer Science, University of Toronto, 1968"},{"key":"9_CR20","volume-title":"Programming in PROLOG","author":"W Clocksin","year":"1981","unstructured":"W. Clocksin, C. Mellish: Programming in PROLOG, Springer 1981"},{"key":"9_CR21","volume-title":"The Algebraic Theory of Semigroups","author":"A Clifford","year":"1961","unstructured":"A. Clifford, G. Preston: \u2018The Algebraic Theory of Semigroups\u2019, vol I and vol II, 1961"},{"key":"9_CR22","volume-title":"Mach. Int","author":"JL Darlington","year":"1971","unstructured":"J.L. Darlington: \u2018A partial Mechanization of Second Order Logic\u2019, Mach. Int. 6, 1971"},{"key":"9_CR23","volume-title":"An Introduction to Database Systems","author":"CJ Date","year":"1976","unstructured":"C.J. Date: \u2018An Introduction to Database Systems\u2019, Addison-Wesley Publ. Comp. Inc., 1976"},{"key":"9_CR24","volume-title":"Amer. Math. Monthly","author":"M Davis","year":"1973","unstructured":"M. Davis: \u2018Hilpert\u2019s tenth Problem is unsolvable\u2019, Amer. Math. Monthly, vol 80, 1973"},{"key":"9_CR25","volume-title":"Proc. of the 2nd Symposium on Symbolic Manipulation","author":"R Fateman","year":"1971","unstructured":"R. Fateman: \u2018The User-Level Semantic Matching Capability in MACSYMA\u2019, Proc. of the 2nd Symposium on Symbolic Manipulation, Los Angeles, 1971"},{"key":"9_CR26","volume-title":"JACM","author":"DJ Farber","year":"1964","unstructured":"D.J. Farber, R.E. Griswald, I.P. Polonsky: \u2018SNOBOL as String Manipulation Language\u2019, JACM, vol 11, no. 2, 1964"},{"key":"9_CR27","first-page":"41","volume-title":"MIT, Project MAC, Report","author":"J Fischer","year":"1974","unstructured":"J. Fischer, S. Patterson: \u2018String Matching and other Products\u2019, MIT, Project MAC, Report 41, 1974"},{"key":"9_CR28","volume-title":"Proc. 4th Workshop on Autom","author":"M Fay","year":"1979","unstructured":"M. Fay: \u2018First Order Unification in an Equational Theory\u2019, Proc. 4th Workshop on Autom. Deduction, Texas, 1979"},{"key":"9_CR29","volume-title":"Private Communication","author":"F Fages","year":"1981","unstructured":"F. Fages: \u2018Private Communication\u2019 (to appear as INRIA report, France), 1981"},{"key":"9_CR30","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1145\/361952.361960","volume":"16","author":"JF Gimpel","year":"1973","unstructured":"J.F. Gimpel: A Theory of Discrete Patterns and their Implementation in SNOBOL4, CACM 16, 2, 1973","journal-title":"CACM"},{"key":"9_CR31","volume-title":"Scientific report no. 4, Air Force Cambridge Research Labs","author":"WE Gould","year":"1966","unstructured":"W.E. Gould: \u2018A matching procedure for \u03c9-order logic\u2019, Scientific report no. 4, Air Force Cambridge Research Labs., 1966"},{"key":"9_CR32","first-page":"710","volume":"AD 602","author":"JR Guard","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","journal-title":"Air Force Cambridge Research Labs."},{"key":"9_CR33","volume-title":"JACM","author":"JR Guard","year":"1969","unstructured":"J.R. Guard, F.C. Oglesby, J.H. Benneth, L.G. Settle: \u2018Semi-Automated Mathematics\u2019, JACM 1969, vol 18, no. 1"},{"key":"9_CR34","first-page":"13","volume-title":"Journal of Theor. Comp. Sci","author":"D Goldfarb","year":"1981","unstructured":"D. Goldfarb: \u2018The Undecidability of the Second Order Unification Problem\u2019, Journal of Theor. Comp. Sci., 13, 1981"},{"key":"9_CR35","doi-asserted-by":"crossref","DOI":"10.1007\/978-0-387-77487-9","volume-title":"Universal Algebra","author":"G Gr\u00e4tzer","year":"1979","unstructured":"G. Gr\u00e4tzer: \u2018Universal Algebra\u2019, Springer Verlag, 1979"},{"key":"9_CR36","volume-title":"Logic and Databases","author":"H Gallaire","year":"1978","unstructured":"H. Gallaire, J. Minker: \u2018Logic and Databases\u2019, Plenum Press, 1978"},{"key":"9_CR37","first-page":"128","volume":"33","author":"J Herbrand","year":"1930","unstructured":"J. Herbrand: \u2018Recherches sour la theorie de la demonstration\u2019, Travaux de la Soc. des Sciences et des Lettres de Varsovie, no. 33, 128, 1930","journal-title":"Travaux de la Soc. des Sciences et des Lettres de Varsovie"},{"key":"9_CR38","volume-title":"R\u00e9solution d\u2019\u00e9quations dans des langages d\u2019ordere","author":"G Huet","year":"1976","unstructured":"G. Huet: \u2018R\u00e9solution d\u2019\u00e9quations dans des langages d\u2019ordere 1,2,...,\u03c9\u2019, Th\u00e8se d\u2019Etat, Univ. de Paris, VII, 1976"},{"key":"9_CR39","volume-title":"Formal Languages: Perspectives and Open Problems","author":"G Huet","year":"1980","unstructured":"G. Huet, D.C. Oppen: \u2018Equations and Rewrite Rules\u2019, in \u201cFormal Languages: Perspectives and Open Problems\u201d, Ed. R. Book, Academic Press, 1980"},{"key":"9_CR40","volume-title":"JACM","author":"G Huet","year":"1980","unstructured":"G. Huet: \u2018Confluent Reductions: Abstract Properties and Applications to Term Rewriting Symstems\u2019, JACM, vol 27, no.4, 1980"},{"key":"9_CR41","volume-title":"Proc. of 5th Workshop on Automated Deduction","author":"JM Hullot","year":"1980","unstructured":"J.M. Hullot: \u2018Canonical Forms and Unification\u2019, Proc. of 5th Workshop on Automated Deduction\u2019, Springer Lecture Notes,1980"},{"key":"9_CR42","doi-asserted-by":"crossref","DOI":"10.21236\/ADA087641","volume-title":"A Catalogue of Canonical Term Rewriting Systems","author":"JM Hullot","year":"1980","unstructured":"J.M. Hullot: \u2018A Catalogue of Canonical Term Rewriting Systems\u2019, Research Rep. CSL-113, SRI-International, 1980"},{"key":"9_CR43","volume-title":"Proc. GWAI-82","author":"A Herold","year":"1982","unstructured":"A. Herold: \u2018Universal Unification and a Class of Equational Theories\u2019, Proc. GWAI-82, W. Wahlster (ed) Springer Fachbe-richte, 1982"},{"key":"9_CR44","volume-title":"Introduction to Semigroup Theory","author":"J Howie","year":"1976","unstructured":"J. Howie: \u2018Introduction to Semigroup Theory\u2019,Acad. Press, 1976"},{"key":"9_CR45","volume-title":"Proc. of the 2nd Symposium on Symbolic Mani-pulation","author":"A Hearn","year":"1971","unstructured":"A. Hearn: \u2018REDUCE2, A System and Language for Algebraic Manipulation\u2019, Proc. of the 2nd Symposium on Symbolic Mani-pulation, Los Angeles, 1971"},{"key":"9_CR46","first-page":"7311","volume-title":"TU M\u00fcnchen, Abtl. Mathematik, Ber. Nr","author":"S Heilbrunner","year":"1973","unstructured":"S. Heilbrunner: \u2018Gleichungssysteme f\u00fcr Zeichenreihen\u2019, TU M\u00fcnchen, Abtl. Mathematik, Ber. Nr. 7311, 1973"},{"key":"9_CR47","volume-title":"Ph. C. Thesis","author":"C Hewitt","year":"1972","unstructured":"C. Hewitt: \u2018Description and Theoretical analysis of PLANNER a language for proving theorems and manipulating models in a robot\u2019, Dept. of Mathematics, Ph. C. Thesis, MIT, 1972"},{"key":"9_CR48","first-page":"92","volume-title":"MIT, AI-Lab., Working paper","author":"C Hewitt","year":"1976","unstructured":"C. Hewitt: \u2018Viewing Control Structures as Patterns of Passing Massages\u2019, MIT, AI-Lab., Working paper 92, 1976"},{"key":"9_CR49","first-page":"724","volume-title":"Dokl. Akad. Nauk SSSR","author":"JI Hmelevskij","year":"1964","unstructured":"J.I. Hmelevskij: \u2018The solution of certain systems of word equations\u2019, Dokl. Akad. Nauk SSSR, 1964, 749 Soviet Math. Dokl.5, 1964, 724"},{"key":"9_CR50","first-page":"1611","volume":"7","author":"JI Hmelevskij","year":"1966","unstructured":"J.I. Hmelevskij: \u2018Word equations without coefficients\u2019, Dokl. Acad. Nauk. SSSR 171, 1966, 1047 Soviet Math. Dokl. 7, 1966, 1611","journal-title":"Dokl. Acad. Nauk. SSSR"},{"key":"9_CR51","volume-title":"Dokl. Akad. Nauk. SSSR","author":"JI Hmelevskij","year":"1967","unstructured":"J.I. Hmelevskij: \u2018Solution of word equations in three unknowns\u2019, Dokl. Akad. Nauk. SSSR 177, 1967, no. 5, Soviet Math. Dokl. 8, 1967, no. 6"},{"key":"9_CR52","volume-title":"Jenning\u2019s Computing Centre rep","author":"GP Huet","year":"1972","unstructured":"G.P. Huet: \u2018Constrained resolution: a complete method for theory\u2019, Jenning\u2019s Computing Centre rep. 1117, Case Western Reserve Univ., 1972"},{"issue":"3","key":"9_CR53","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1016\/S0019-9958(73)90301-X","volume":"22","author":"GP Huet","year":"1973","unstructured":"G.P. Huet: \u2018The undecidability of unification in third order logic\u2019, Information and Control 22 (3), 257\u2013267, 1973","journal-title":"Information and Control"},{"key":"9_CR54","volume-title":"\u03bb-Calculus and Comp. Sci. Theory","author":"G Huet","year":"1975","unstructured":"G. Huet: \u2018Unification in typed Lambda Calculus\u2019, in \u03bb-Calculus and Comp. Sci. Theory, Springer Lecture Notes, No. 37, Proc. of the Symp. held in Rome, 1975"},{"key":"9_CR55","first-page":"1","volume-title":"J. Theor. Comp. Sci","author":"GP Huet","year":"1975","unstructured":"G.P. Huet: \u2018A Unification Algorithm for typed \u03bb-Calculus\u2019, J. Theor. Comp. Sci., 1, 1975"},{"key":"9_CR56","volume-title":"Rep. CS73-16","author":"D Jensen","year":"1973","unstructured":"D. Jensen, T.Pietrzykowski: \u2018Mechanising \u03c9-order type theory through unification\u2019, Rep. CS73-16, Dept. of Applied Analysis and Comp. Sci. University of Waterloo, 1973"},{"key":"9_CR57","first-page":"4","volume-title":"ACM Symposium on Th. of Comp","author":"Karp","year":"1972","unstructured":"Karp, Miller, Rosenberg: \u2018Rapid Identification of repeated Patterns in Strings, Trees and Arrays\u2019, ACM Symposium on Th. of Comp. 4, 1972"},{"key":"9_CR58","volume-title":"Computational Problems in Abstract Algebra","author":"DE Knuth","year":"1970","unstructured":"D.E. Knuth, P.B. Bendix: \u2018Simple word Problems in Unviersal Algebras\u2019, in: Computational Problems in Abstract Algebra, J. Leech (ed), Pergamon Press, Oxford, 1970"},{"key":"9_CR59","volume-title":"Stan-CS-74-44O","author":"Knuth","year":"1974","unstructured":"Knuth, Morris, Pratt: \u2018Fast Pattern Matching in Strings\u2019, Stan-CS-74-44O, Stanford University, Comp. Sci. Dept., 1974"},{"key":"9_CR60","volume-title":"Proceedings of fourth IJCAI","author":"S K\u00fchner","year":"1977","unstructured":"S. K\u00fchner, Ch. Mathis, P. Raulefs, J. Siekmann: \u2018Unification of Ideitipotent Functions\u2019, Proceedings of fourth IJCAI, MIT, Cambridge, 1977"},{"key":"9_CR61","volume-title":"Logic for Problem Solving","author":"R Kowalski","year":"1979","unstructured":"R. Kowalski: \u2018Logic for Problem Solving\u2019, North Holland, 1979"},{"key":"9_CR62","volume-title":"General Electric","author":"D Kapur","year":"1982","unstructured":"D. Kapur, M.S. Krishnamoorthy, P. Narendran: \u2018A new linear Algorithm for Unification\u2019, General Electric, Rep. no. 82CRD-1oo, New York, 1982"},{"key":"9_CR63","volume-title":"Nota Interna","author":"G Levi","year":"1973","unstructured":"G. Levi, F. Sirovich: \u2018Pattern Matching and Goal directed Computation\u2019, Nota Interna B73-12, Univ. of Pisa, 1973"},{"key":"9_CR64","volume-title":"Rep. CSRR 2059","author":"CL Lucchesi","year":"1972","unstructured":"C.L. Lucchesi: \u2018The undecidability of the unification problem for third order languages\u2019, Rep. CSRR 2059, Dept. of Applied Analysis and Comp. Science, Univ. of Waterloo, 1972"},{"key":"9_CR65","volume-title":"A new complete FPA-Unification Algorithm","author":"DS Lankford","year":"1980","unstructured":"D.S. Lankford: \u2018A new complete FPA-Unification Algorithm\u2019, MIT-8, Louisiana Techn. Univ., 1980"},{"key":"9_CR66","volume-title":"A Unification Algorithm for Abelian Group Theory","author":"DS Lankford","year":"1979","unstructured":"D.S. Lankford: \u2018A Unification Algorithm for Abelian Group Theory\u2019, Rep. MTP-1, Louisiana Techn. Univ., 1979"},{"key":"9_CR67","volume-title":"4th Workshop on Autom","author":"DS Lankford","year":"1979","unstructured":"D.S. Lankford, M. Ballantyne: \u2018The Refutation Completeness of Blocked Permutative Narrowing and Resolution\u2019, 4th Workshop on Autom. Deduction, Texas, 1979"},{"key":"9_CR68","volume-title":"Termination and Decidability Results for Stringunification","author":"M Livesey","year":"1975","unstructured":"M. Livesey, J. Siekmann: \u2018Termination and Decidability Results for Stringunification\u2019, Univ. of Essex, Memo CSM-12, 1975"},{"key":"9_CR69","volume-title":"Unification of Sets and Multisets","author":"M Livesey","year":"1976","unstructured":"M. Livesey, J. Siekmann: \u2018Unification of Sets and Multisets\u2019, Univ. Karlsruhe, Techn. Report, 1976"},{"key":"9_CR70","volume-title":"Automated Theorem Proving","author":"D Loveland","year":"1980","unstructured":"D. Loveland: \u2018Automated Theorem Proving\u2019, North Holland, 1980"},{"key":"9_CR71","volume-title":"Proc. of Conf. on Autom. Deduction","author":"M Livesey","year":"1979","unstructured":"M. Livesey, J. Siekmann, P. Szab\u00f3, E. Unvericht: \u2018Unification Problems for Combinations of Associativity, Commutativity, Distributivity and Idempotence Axioms\u2019, Proc. of Conf. on Autom. Deduction, Austin, Texas, 1979"},{"key":"9_CR72","volume-title":"The Problem of Solvability of Equations in a Free Semigroup","author":"GS Makanin","year":"1977","unstructured":"G.S. Makanin: \u2018The Problem of Solvability of Equations in a Free Semigroup\u2019, Soviet Akad. Nauk SSSR, Tom 233, no. 2, 1977"},{"key":"9_CR73","volume-title":"An Efficient Unification Algorithm","author":"A Martelli","year":"1979","unstructured":"A. Martelli, U. Montaneri: \u2018An Efficient Unification Algorithm\u2019, University of Pisa, Techn. Report, 1979"},{"key":"9_CR74","volume-title":"Proc. of the Scand. Logic Symp","author":"Y Matiyasevich","year":"1978","unstructured":"Y. Matiyasevich: \u2018Diophantine Representation of Rec. Enumerable Predicates\u2019, Proc. of the Scand. Logic Symp., North Holland, 1978"},{"key":"9_CR75","volume-title":"IFIP Conf. on Symb","author":"Manove","year":"1968","unstructured":"Manove, Bloom, Engelmann: \u2018Rational Functions in MATHLAB\u2019, IFIP Conf. on Symb. Manipulation, Pisa, 1968"},{"key":"9_CR76","first-page":"1038","volume":"17","author":"AA Markov","year":"1954","unstructured":"A.A. Markov: \u2018Trudy Mat. Inst. Steklov\u2019, no. 42, Izdat. Akad. Nauk SSSR, 1954, NR 17, 1038, 1954","journal-title":"Izdat. Akad. Nauk SSSR"},{"key":"9_CR77","volume-title":"Graphs as Strings","author":"Maurer","year":"1977","unstructured":"Maurer: \u2018Graphs as Strings\u2019, Universit\u00e4t Karlsruhe, Techn. Rep., 1977"},{"key":"9_CR78","first-page":"8","volume":"14","author":"J Moses","year":"1971","unstructured":"J. Moses: Symbolic Integration: \u2018The Stormy Decade\u2019, CACM 14, 8, 1971","journal-title":"The Stormy Decade"},{"key":"9_CR79","volume-title":"Project MAC","author":"J Moses","year":"1974","unstructured":"J. Moses: \u2018MACSYMA -the fifth Year\u2019, Project MAC, MIT, Cambridge, 1974"},{"key":"9_CR80","volume-title":"Principles of Artificial Intelligence","author":"N Nilsson","year":"1980","unstructured":"N. Nilsson: \u2018Principles of Artificial Intelligence\u2019, Tioga Publ. Comp., Cal., 1980"},{"key":"9_CR81","first-page":"21","volume-title":"JACM","author":"A Nevins","year":"1974","unstructured":"A. Nevins: \u2018A Human oriented logic for ATP\u2019, JACM 21, 1974 (first report 1971)"},{"key":"9_CR82","first-page":"16","volume-title":"J. of Comp. and Syst. Science","author":"M Paterson","year":"1968","unstructured":"M. Paterson, M. Wegman: \u2018Linear Unification\u2019, J. of Comp. and Syst. Science, 1968, 16"},{"key":"9_CR83","first-page":"26","volume-title":"Theoria","author":"D Prawitz","year":"1960","unstructured":"D. Prawitz: \u2018An Improved Proof Procedure\u2019, Theoria 26, 1960"},{"key":"9_CR84","volume-title":"JACM","author":"G Peterson","year":"1981","unstructured":"G. Peterson, M. Stickel: \u2018Complete Sets of Reductions for Equational Theories with Complete Unification Algorithms\u2019, JACM, vol 28, no. 2, 1981"},{"key":"9_CR85","first-page":"7","volume-title":"Machine Intelligence","author":"G Plotkin","year":"1972","unstructured":"G. Plotkin: \u2018Building in Equational Theories\u2019, Machine Intelligence, vol 7, 1972"},{"key":"9_CR86","volume-title":"Unification of Idempotent Functions","author":"P Raulefs","year":"1978","unstructured":"P. Raulefs, J. Siekmann: \u2018Unification of Idempotent Functions\u2019, Universit\u00e4t Karlsruhe, Techn. Report, 1978"},{"key":"9_CR87","first-page":"13","volume-title":"SIGSAM Bulletin","author":"P Raulefs","year":"1979","unstructured":"P. Raulefs, J. Siekmann, P. Szab\u00f3, E. Unvericht: A short Survey on the State of the Art in Matching and Unification Problems, SIGSAM Bulletin, 13, 1979"},{"key":"9_CR88","first-page":"12","volume-title":"JACM","author":"JA Robinson","year":"1965","unstructured":"J.A. Robinson: \u2018A Machine Oriented Logic based on the Resolution Principle\u2019, JACM 12, 1965"},{"key":"9_CR89","first-page":"6","volume-title":"Machine Intelligence","author":"JA Robinson","year":"1971","unstructured":"J.A. Robinson: \u2018Computational Logic: The Unification Compu-tation\u2019, Machine Intelligence, vol 6, 1971"},{"key":"9_CR90","volume-title":"Graph-family Matching","author":"J Rastall","year":"1969","unstructured":"J. Rastall: \u2018Graph-family Matching\u2019, Univers. of Edinburgh, MIP-R-62, 1969"},{"key":"9_CR91","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1090\/psapm\/019\/0241195","volume":"19","author":"JA Robinson","year":"1967","unstructured":"J.A. Robinson: \u2018A review on automatic theorem proving\u2019, Symp. Appl. Math., vol 19, 1\u201318, 1967","journal-title":"Symp. Appl. Math."},{"key":"9_CR92","volume-title":"QA4: A procedural calculus for intuitive reasoning","author":"Rulifson","year":"1972","unstructured":"Rulifson, Derksen, Waldinger: \u2018QA4: A procedural calculus for intuitive reasoning\u2019, Stanford Univ., Nov. 1972"},{"key":"9_CR93","volume-title":"Stringunification","author":"J Siekmann","year":"1975","unstructured":"J. Siekmann: \u2018Stringunification\u2019 Essex University, Memo CSM-7, 1975"},{"key":"9_CR94","volume-title":"Unification of Commutative Terms","author":"J Siekmann","year":"1976","unstructured":"J. Siekmann: \u2018Unification of Commutative Terms\u2019, Universit\u00e4t Karlsruhe, 1976 (full paper submitted)"},{"key":"9_CR95","unstructured":"J. Siekmann: \u2018Unification and Matching Problems\u2019, Ph.D., Essex University, MEMO CSM-4-78"},{"key":"9_CR96","volume-title":"Universal Unification and Regular ACFM Theories","author":"J Siekmann","year":"1981","unstructured":"J. Siekmann, P. Szab\u00f3: \u2018Universal Unification and Regular ACFM Theories\u2019, Proc. IJCAI-81, Vancouver, 1981 (full paper submitted)"},{"key":"9_CR97","volume-title":"Semigroup Forum","author":"J Siekmann","year":"1982","unstructured":"J. Siekmann, P. Szab\u00f3: \u2018A Noetherian and Confluent Rewrite System for Idempotent Semigroups\u2019, Semigroup Forum, vol 25, 1982"},{"key":"9_CR98","volume-title":"Proc. of Conf. on Autom. Deduction","author":"J Siekmann","year":"1982","unstructured":"J. Siekmann, P. Szab\u00f3: \u2018Universal Unification and a Classific-ation of Equational Theories\u2019, Proc. of Conf. on Autom. Deduction, 1982, New York, Springer Lecture Notes Comp. Sci., vol 87 (full paper submitted)"},{"key":"9_CR99","volume-title":"A Minimal Unification Algorithm for Idempotent Functions","author":"J Siekmann","year":"1982","unstructured":"J. Siekmann, P. Szab\u00f3: \u2018A Minimal Unification Algorithm for Idempotent Functions\u2019, Universit\u00e4t Karlsruhe, 1982 (in preparation)"},{"key":"9_CR100","volume-title":"Undecidability of the DA-Unification Problem","author":"P Szab\u00f3","year":"1979","unstructured":"P. Szab\u00f3: \u2018Undecidability of the DA-Unification Problem\u2019, Proc. of GWAI, 1979 (full paper submitted)"},{"key":"9_CR101","volume-title":"Theory of First Order Unification","author":"P Szab\u00f3","year":"1982","unstructured":"P. Szab\u00f3: Theory of First Order Unification (in German, thesis), Universit\u00e4t Karlsruhe, 1982"},{"key":"9_CR102","volume-title":"The Unification Problem for Distributive Terms","author":"P Szabo","year":"1978","unstructured":"P. Szabo, E. Unvericht: \u2018The Unification Problem for Distributive Terms\u2019, Universit\u00e4t Karlsruhe, 1978"},{"key":"9_CR103","volume-title":"Paramodulation and Unification","author":"P Szab\u00f3","year":"1982","unstructured":"P. Szab\u00f3: \u2018Paramodulation and Unification\u2019, Universit\u00e4t Karlsruhe, 1982 (in preparation)"},{"key":"9_CR104","first-page":"21","volume-title":"JACM","author":"J Slagle","year":"1974","unstructured":"J. Slagle: \u2018ATP for Theories with Simplifiers, Commutativity and Associativity\u2019, JACM 21, 1974"},{"key":"9_CR105","volume-title":"JACM","author":"M Stickel","year":"1981","unstructured":"M. Stickel: \u2018A Unification Algorithm for Assoc. Commutative Functions\u2019, JACM, vol 28, no. 3, 1981"},{"key":"9_CR106","volume-title":"MYCIN: Computer Based Medical Consultations","author":"EH Shortliffe","year":"1976","unstructured":"E.H. Shortliffe: \u2018MYCIN: Computer Based Medical Consultations\u2019, North Holland Publ. Comp. 1976"},{"key":"9_CR107","volume-title":"Z. Math. Logic Grundlagen","author":"D Skordew","year":"1961","unstructured":"D. Skordew, B. Sendow: \u2018Z. Math. Logic Grundlagen\u2019, Math. 7 (1961), 289, MR 31, 57 (Russian) (English translation at University of Essex, Comp. Sci. Dept.)"},{"key":"9_CR108","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1145\/321679.321689","volume":"19","author":"JR Slagle","year":"1972","unstructured":"J.R. Slagle: \u2018ATP with built-in theories including equality, partial ordering and sets\u2019, JACM 19, 120\u2013135, 1972","journal-title":"JACM"},{"key":"9_CR109","volume-title":"A Plasma Primer","author":"BC Smith","year":"1975","unstructured":"B.C. Smith, C. Hewitt: \u2018A Plasma Primer\u2019, MIT, AI-Lab., 1975"},{"key":"9_CR110","volume-title":"An Algebraic Model for String Patterns","author":"GF Stewart","year":"1974","unstructured":"G.F. Stewart: \u2018An Algebraic Model for String Patterns\u2019, University of Toronto, CSRG-39, 1974"},{"key":"9_CR111","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1021\/c160016a007","volume":"5","author":"E Sussenguth","year":"1965","unstructured":"E. Sussenguth: \u2018A graph-theoretical algorithm for matching chemical structures\u2019, J. Chem. Doc. 5, 1, 1965","journal-title":"J. Chem. Doc."},{"key":"9_CR112","volume-title":"CM special interest group on Symbolic and Algebraic Manipulation","author":"SIGSAM Bulletin","year":"1977","unstructured":"SIGSAM Bulletin: \u2018ACM special interest group on Symbolic and Algebraic Manipulation\u2019, vol 11, no. 3, 1977 (issue no. 43) contains an almost complete bibliography"},{"key":"9_CR113","volume-title":"Petrocelli Books","author":"H Tennant","year":"1981","unstructured":"H. Tennant: \u2018Natural Language Processing\u2019, Petrocelli Books, 1981"},{"key":"9_CR114","volume-title":"Contributions to Mathematical Logic","author":"A Tarski","year":"1968","unstructured":"A. Tarski: \u2019Equational Logic and Equational Theories of Algebra\u2019, Schmidt et al (eds), Contributions to Mathematical Logic, North Holland, 1968"},{"key":"9_CR115","volume-title":"Colloquia Mathematica Societatis Janos Bolya","author":"W Taylor","year":"1975","unstructured":"W. Taylor: \u2018Equational Logic\u2019, Colloquia Mathematica Societatis Janos Bolya, 1975"},{"key":"9_CR116","first-page":"1","volume-title":"JACM","author":"JR Ullman","year":"1976","unstructured":"J.R. Ullman: \u2018An Algorithm for Subgraph Isomorphism\u2019, JACM, vol 23, no.1, 1976"},{"key":"9_CR117","first-page":"1","volume-title":"CACM","author":"SH Unger","year":"1964","unstructured":"S.H. Unger: \u2018GIT -A Heuristic Program for Testing Pairs of directed Line Graphs for Isomorphism\u2019, CACM, vol 7, no. 1, 1964"},{"key":"9_CR118","volume-title":"Proc. of Fourth IJCAI","author":"J Vaalen van","year":"1975","unstructured":"J. van Vaalen: \u2018An Extension of Unification to Substitutions with an Application to ATP\u2019, Proc. of Fourth IJCAI, Tbilisi, USSR, 1975"},{"key":"9_CR119","volume-title":"Unifikation von Morphismen","author":"E Vogel","year":"1978","unstructured":"E. Vogel: \u2018Unifikation von Morphismen\u2019, Diplomarbeit, Univer-sit\u00e4t Karlsruhe, 1978"},{"key":"9_CR120","volume-title":"mplementing PROLOG","author":"DHD Warren","year":"1977","unstructured":"D.H.D. Warren: \u2018Implementing PROLOG\u2019, vol 1 and vol 2, D.A.I. Research Rep., no. 39, University of Edinburgh, 1977"},{"key":"9_CR121","first-page":"14","volume-title":"IEEE Symp. on Sw. and Automata Theory","author":"P Weiner","year":"1973","unstructured":"P. Weiner: \u2018Linear Pattern Matching Algorithms\u2019, IEEE Symp. on Sw. and Automata Theory, 14, 1973"},{"key":"9_CR122","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-95279-1","volume-title":"Revised Rep. on the Algorithmic Language ALGOL68","author":"Wijngaarden van","year":"1976","unstructured":"van Wijngaarden (et al): \u2018Revised Rep. on the Algorithmic Language ALGOL68\u2019, Springer-Verlag, Berlin, Heidelberg, N.Y., 1976"},{"key":"9_CR123","volume-title":"he Psychology of Computer Vision","author":"Winston","year":"1975","unstructured":"Winston: \u2018The Psychology of Computer Vision\u2019, McGraw Hill, 1975"},{"key":"9_CR124","volume-title":"Unification in Second Order Logic","author":"G Winterstein","year":"1976","unstructured":"G. Winterstein: \u2018Unification in Second Order Logic\u2019, Bericht 3, Universit\u00e4t Kaiserslautern, 1976"},{"key":"9_CR125","first-page":"1","volume-title":"JACM","author":"K Wong","year":"1976","unstructured":"K. Wong, K. Chandra: \u2018Bounds for the String Editing Problem\u2019, JACM, vol 23, no. 1, 1976"},{"key":"9_CR126","volume-title":"Word problems","author":"L Wos","year":"1973","unstructured":"L. Wos, G. Robinson: \u2018Maximal Models and Refutation Completeness: Semidecision Procedures in A-utomatic Theorem Proving\u2019, in: Word problems (W.W. Boone, F.B. Cannonito, R.C. Lyndon, eds), North Holland, 1973"},{"key":"9_CR127","first-page":"4","volume-title":"JACM","author":"L Wos","year":"1967","unstructured":"L. Wos, G.A. Robinson, D. Carson, L. Shalla: \u2018The Concept of Demodulation in Theorem Proving\u2019, JACM, vol 14, no. 4, 1967"},{"key":"9_CR128","volume-title":"Treatise on Universal Algebra","author":"N Whitehead","year":"1898","unstructured":"N. Whitehead: \u2018Treatise on Universal Algebra\u2019, 1898"}],"container-title":["Informatik-Fachberichte","GWAI-82"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-68826-3_9.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,10]],"date-time":"2023-06-10T20:35:51Z","timestamp":1686429351000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-68826-3_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1982]]},"ISBN":["9783540119609","9783642688263"],"references-count":128,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-68826-3_9","relation":{},"ISSN":["0343-3005"],"issn-type":[{"type":"print","value":"0343-3005"}],"subject":[],"published":{"date-parts":[[1982]]}}}