A short survey on the state of the art in matching and unification problems

ABSTRACT

1. Motivations There is a wide variety of areas where matching and unification problems arise: (1.1) Databases The user of a (relational) database [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].

REFERENCES

• 1: A. Ballantyne, D. Lankford; 'Decision Procedures for simple equational theories', University of Texas at Austin, ATP-35, ATP-37, ATP-39, 1977
• 2: Barrow, Ambler, Burstall; 'Some techniques for recognizing Structures in Pictures', Frontiers of Pattern Recognition, Academic Press Inc., 1972
• 3: L.D. Baxter; 'An efficient Unification Algorithm', Rep. CS-73-23, University of Waterloo, Dept. of Analysis and Computer Science, 1973
• 4: Bennett, Easton, Guard, Settle; 'CRT-aided semiautomated mathematics', AFCRL-63, Applied Logic Corp., 1963
• 5: Bennett, Easton; 'CRT-aided semi-automated mathematics', AFCRL-65, Applied Logic Corporation, 1965
• 6: Bennett, Easton, Guard, Settle; 'CRT-aided semi-automated mathematics', AFCRL-67-0167. Applied Corp., Princeton
• 7: J. H. Griesmer , R. D. Jenks, SCRATCHPAD/1: An interactive facility for symbolic mathematics, Proceedings of the second ACM symposium on Symbolic and algebraic manipulation, p.42-58, March 23-25, 1971, Los Angeles, California, United States [doi>10.1145/800204.806266]
• 8: D. G. Bobrow (ed.); 'Symbol Manipulation Languages', Proc. of IFIP, North Holland Publishing Comp., 1968
• 9: H. P. Böhm , H. L. Fischer , P. Raulefs, CSSA: Language concepts and programming methodology, Proceedings of the 1977 symposium on Artificial intelligence and programming languages, p.100-108, August 15-17, 1977
• 10: H. Boley; 'Directed Recursive Labelnode Hypergraphs: A New Representation Language', Journal of Artificial Intelligence, vol 9, no. 1, 1977
• 11: H. Bryan, J. Carnog; 'Search methods used with transistor patent applications', IEEE Spectrum 3, 2, 1966
• 12: B. F. Caviness, On Canonical Forms and Simplification, Journal of the ACM (JACM), v.17 n.2, p.385-396, April 1970 [doi>10.1145/321574.321591]
• 13: Carlos Christensen , Michael Karr, IAM, a system for interactive algebraic manipulation, Proceedings of the second ACM symposium on Symbolic and algebraic manipulation, p.115-127, March 23-25, 1971, Los Angeles, California, United States [doi>10.1145/800204.806276]
• 14: M. Clowes; 'On Seeing Things', Journal of Artificial Intelligence, 1971
• 15: CODASYL Systems Committee; 'A survey of Generalized Data Base Management Systems', Techn. Rep. 1969, ACM and IAG
• 16: CODASYL Systems Committee; 'Feature Analysis of Generalized Data Base Management Systems', TR 1971, ACM, BC and IAG
• 17: E. F. Codd, A relational model of data for large shared data banks, Communications of the ACM, v.13 n.6, p.377-387, June 1970 [doi>10.1145/362384.362685]
• 18: E. F. Codd; 'Relational Completeness of Data Base Sublanguages', in Data Base Systems, Prentice Hall, Courant Comp. Science Symposia Series, vol 6, 1972
• 19: Cook; 'Algebraic techniques and the mechanization of number theory', RM-4319-PR, Rand Corp., Santa Monica, Cal., 1965
• 20: D. G. Corneil; 'Graph Isomorphism', Ph. D. Dept. of Computer Science, University of Toronto, 1968
• 21: J. L. Darlington; 'A partial Mechanization of Second Order Logic', Mach. Int. 6, 1971
• 22: C. J. Date, An Introduction to Database Systems, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1991
• 23: Richard J. Fateman, The user-level semantic matching capability in MACSYMA, Proceedings of the second ACM symposium on Symbolic and algebraic manipulation, p.311-323, March 23-25, 1971, Los Angeles, California, United States [doi>10.1145/800204.806300]
• 24: D. J. Farber , R. E. Griswold , I. P. Polonsky, SNOBOL , A String Manipulation Language, Journal of the ACM (JACM), v.11 n.1, p.21-30, Jan. 1964 [doi>10.1145/321203.321207]
• 25: M. J. Fischer , M. S. Paterson, STRING-MATCHING AND OTHER PRODUCTS, Massachusetts Institute of Technology, Cambridge, MA, 1974
• 26: J. F. Gimpel, A theory of discrete patterns and their implementation in SNOBOL4, Communications of the ACM, v.16 n.2, p.91-100, Feb. 1973 [doi>10.1145/361952.361960]
• 27: W. E. Gould; 'A matching procedure for ω-order logic', Scientific report No. 4, Air Force Cambridge Research Labs., 1966
• 28: J. R. Guard; 'Automated logic for semi automated mathematics', Scientific report No. 1, Air Force Cambridge Research Labs., AD 602 710, 1964
• 29: Anthony C. Hearn, REDUCE 2: A system and language for algebraic manipulation, Proceedings of the second ACM symposium on Symbolic and algebraic manipulation, p.128-133, March 23-25, 1971, Los Angeles, California, United States [doi>10.1145/800204.806277]
• 30: S. Heilbrunner; 'Gleichungssysteme für Zeichenreihen', TU München, Abtl. Mathematik, Ber. Nr. 7311, 1973
• 31: C. Hewitt; 'Description and Theoretical analysis of PLANNER a language for proving theorems and manipulating models in a robot', Dept. of Mathematics, Ph.D. Thesis, MIT, 1972
• 32: C. Hewitt; 'Viewing Control Structures as Patterns of Passing Massages', MIT, AI-Lab., Working paper 92, 1976
• 33: J. I. Hmelevskij; 'The solution of certain systems of word equations', Dokl. Akad. Nauk SSSR, 1964, 749 Soviet Math. Dokl. 5, 1964, 724
• 34: J. I. Hmelevskij; 'Word equations without coefficients', Dokl. Akad. Nauk. SSSR 171, 1966, 1047 Soviet Math. Dokl.7, 1966, 1611
• 35: 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
• 36: G. P. Huet; 'Constrained resolution: a complete method for theory', Jenning's Computing Centre rep. 1117, Case Western Reserve Univ., 1972
• 37: G. P. Huet; 'The undecidability of unification in third order logic', Information and Control 22 (3), 257--267, 1973
• 38: Gérard P. Huet, unification in typed lambda calculus, Proceedings of the Symposium on Lambda-Calculus and Computer Science Theory, p.192-212, March 25-27, 1975
• 39: G. P. Huet; 'A Unification Algorithm for typed λ-Calculus', J. Theor. Comp. Sci., 1, 1975
• 40: G. Huet; 'Résolution d'équations dans des langages d'ordre 1..2,..., w; Thèse d'etat, IRIA-Laboria, 1976
• 41: G. Huet; 'Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems', IRIA-Laboria, Rap. de Recherche no. 250, Rocquencourt, 1977
• 42: D. Jensen, T. Pietrzykowski; 'Mechanising ω-order type theory through unification', Rep. CS-73-16, Dept. of Applied Analysis and Comp. Sci. University of Waterloo, 1973
• 43: Richard M. Karp , Raymond E. Miller , Arnold L. Rosenberg, Rapid identification of repeated patterns in strings, trees and arrays, Proceedings of the fourth annual ACM symposium on Theory of computing, p.125-136, May 01-03, 1972, Denver, Colorado, United States [doi>10.1145/800152.804905]
• 44: 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
• 45: Knuth, Morris, Pratt; 'Fast Pattern Matching in Strings', Stan-CS-74-440, Stanford University, Comp. Sci. Dept., 1974
• 46: S. Kühner, Ch. Mathis, P. Raulefs, J. Siekmann; 'Unification of Idempotent Functions', Proceedings of fourth IJCAI-77, MIT, Cambridge
• 47: G. Levi, F. Sirovich; 'Pattern Matching and Goal directed Computation', Nota Interna B73-12, Univ. of Pisa, 1973
• 48: M. Livesey, J. Siekmann; 'Termination and Decidability Results for String Unification', Essex University, Computer Centre Memo CSM-12, 1975
• 49: M. Livesey, J. Siekmann; 'Unification of Sets', Int. Ber. 3/76, Inst. f. Informatik I, Univ. Karlsruhe
• 50: 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
• 51: G. S. Makanin; 'The Problem of Solvability of Equations in a Free Semigroup', Soviet. Akad. Nauk SSSR, TOM 233, no. 2, 1977
• 52: Manove, Bloom, Engelmann; 'Rational Functions in MATHLAB', IFIP Conf. on Symb. Manip., Pisa, 1968
• 53: A. A. Markov; 'Trudy Mat. Inst. Steklov', No. 42, Izdat. Akad. Nauk SSSR, 1954, MR 17, 1038, 1954
• 54: Maurer; 'Graphs as Strings', Universität Karlsruhe, Techn. Report, 1977
• 55: Joel Moses, Symbolic integration: the stormy decade, Communications of the ACM, v.14 n.8, p.548-560, Aug. 1971 [doi>10.1145/362637.362651]
• 56: J. Moses; 'MACSYMA - the fifth Year', Project MAC, MIT, Cambridge, 1974
• 57: A. Nevins; 'A human-oriented logic for automatic theorem proving', George Washington University, Techn. Rep., 1971
• 58: Paterson, Wegman; 'Linear Unification', IBM Research Report 5304, 1976
• 59: G. E. Peterson, M. E. Stickel; 'Complete Sets of Reductions for Equational Theories with Complete Unification Algorithms', University of Arizona, Techn. Rep., 1978
• 60: G. Plotkin; 'Building in equational theories', Mach. Intelligence, vol 7, 1972
• 61: J. Rastall; 'Graph-family Matching', Univ. of Edinburgh, MIP-R-62, 1969
• 62: P. Raulefs, J. Siekmann; 'Unification of Idempotent Functions', (extended and revised version of {46}, 1978
• 63: J. A. Robinson, A Machine-Oriented Logic Based on the Resolution Principle, Journal of the ACM (JACM), v.12 n.1, p.23-41, Jan. 1965 [doi>10.1145/321250.321253]
• 64: J. A. Robinson; 'A review on automatic theorem proving', Symp. Appl. Math., vol 19, 1--18, 1967
• 65: J. A. Robinson; 'Computational Logic: The Unification Computation', Mach. Intell. 6, 1970
• 66: 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
• 67: Johns Frederick Rulifson, Language-qa4: a procedural calculus for intuitive reasoning., 1973
• 68: This interesting area of application was pointed out to us by W. Schönfeld, Universität Stuttgart
• 69: J. Siekmann; 'Stringunification' Essex University, Memo CSM-7, 1975
• 70: J. Siekmann; 'Unification of commutative terms', Universität Karlsruhe. Int. Bericht 2, 1976
• 71: J. Siekmann; 'Unification and Matching Problems', Ph.D., Essex University, MEMO CSM-4-78
• 72: SIGSAM Bulletin; 'ACM special interest group on Symbolic and Algebraic Manipulation', vol 11, no. 3, 1977 (issue no. 43) contains an almost complete bibliography
• 73: 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.)
• 74: James R. Slagle, Automatic Theorem Proving with Built-in Theories Including Equality, Partial Ordering, and Sets, Journal of the ACM (JACM), v.19 n.1, p.120-135, Jan. 1972 [doi>10.1145/321679.321689]
• 75: James R. Slagle, Automated Theorem-Proving for Theories with Simplifiers Commutativity, and Associativity, Journal of the ACM (JACM), v.21 n.4, p.622-642, Oct. 1974 [doi>10.1145/321850.321859]
• 76: B. C. Smith, C. Hewitt; 'A Plasma Primer', MIT, AI-Lab., 1975
• 77: G. F. Stewart; 'An Algebraic Model for String Patterns', University of Toronto, CSRG-39, 1974
• 78: M. E. Stickel; 'A complete unification algorithm for associative, commutative Functions', Proc. 4th IJCAI, Tbilis, USSR, 1975
• 79: E. Sussenguth; 'A graph-theoretical algorithm for matching chemical structures', J. Chem. Doc. 5, 1, 1965
• 80: P. Szabó; 'The Undecidability of the DA-Unification Problem; Universität Karlsruhe, Int. Ber. 3, 1978
• 81: P. Szabó, E. Unvericht; 'D-Unification has infinitely many mgus', Universität Karlsruhe, Inst. f. Informatik I (forthcoming)
• 82: J. R. Ullmann, An Algorithm for Subgraph Isomorphism, Journal of the ACM (JACM), v.23 n.1, p.31-42, Jan. 1976 [doi>10.1145/321921.321925]
• 83: Stephen H. Unger, GIT—a heuristic program for testing pairs of directed line graphs for isomorphism, Communications of the ACM, v.7 n.1, p.26-34, Jan. 1964 [doi>10.1145/363872.363899]
• 84: J. van Vaalen; 'An Extension of Unification to Substitutions with an Application to ATP', Proc. of Fourth IJCAI, Tbilisi, USSR, 1975
• 85: E. Vogel; 'Unifikation von Morphismen', Diplomarbeit, forthcoming, 1978
• 86: D. H. D. Warren; 'Implementing PROLOG', vol 1 and vol 2, D.A.I. Research Rep. no. 39, University of Edinburgh, 1977
• 87: P. Weiner; 'Linear Pattern Matching Algorithms', IEEE Symp. on Sw. and Automata Theory, 14, 1973
• 88: A. van Wijngaarden, Report on the algorithmic language ALGOL 68, Printing by the Mathematisch Centrum, 1969
• 89: Winston; 'The Psychology of Computer Vision', 1975, McGraw Hill
• 90: G. Winterstein; 'Unification in Second Order Logic', Bericht 3, Univ. Kaiserslautern, 1976
• 91: C. K. Wong , Ashok K. Chandra, Bounds for the String Editing Problem, Journal of the ACM (JACM), v.23 n.1, p.13-16, Jan. 1976 [doi>10.1145/321921.321923]