Matching, unification and complexity

ABSTRACT

Pattern matching and unification are two key primitive operations used in many inference based systems including theorem provers, term rewriting systems, computer algebra systems, deductive data bases, Prolog, logic programming systems, functional language systems, systems for analysis of specifications and program synthesis, and program verification systems. In this note, we give results recently obtained in studying the complexity of matching and unification problems for first-order terms especially when some function symbols are interpreted. For further details and proofs, the reader may wish to refer to a forthcoming paper by the authors.

REFERENCES

• 1: Stefan Arnborg , Erik Tidén, Unification Problems with One-Sided Distributivity, Proceedings of the First International Conference on Rewriting Techniques and Applications, p.398-406, May 20-22, 1985
• 2: Dan Benanav , Deepak Kapur , Paliath Narendran, Complexity of Matching Problems, Proceedings of the First International Conference on Rewriting Techniques and Applications, p.417-429, May 20-22, 1985
• 3: {CK} Chandra, A., and Kanellakis, P., personal communication, 1985.
• 4: Michael R. Garey , David S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, W. H. Freeman & Co., New York, NY, 1979
• 5: Abdelilah Kandri-Rody , Deepak Kapur , Paliath Narendran, An Ideal-Theoretic Approach to Work Problems and Unification Problems over Finitely Presented Commutative Algebras, Proceedings of the First International Conference on Rewriting Techniques and Applications, p.345-364, May 20-22, 1985
• 6: Deepak Kapur , Paliath Narendran, NP-Completeness of the Set Unification and Matching Problems, Proceedings of the 8th International Conference on Automated Deduction, p.489-495, July 27-August 01, 1986
• 7: {KN862} Kapur, D., and Narendran, P., "NP-completeness of the associative-commutative unification and related problems," Unpublished Manuscript, Computer Science Branch, General Electric Corporate Research and Development, Schenectady, NY, Dec. 1986.
• 8: Deepak Kapur , Paliath Narendran, Matching, unification and complexity, ACM SIGSAM Bulletin, v.21 n.4, p.6-9, Nov. 1987 [doi>10.1145/36330.36332]
• 9: Dexter Kozen, Complexity of Finitely Presented Algebras, Cornell University, Ithaca, NY, 1976
• 10: {PW} Paterson, M. S., and Wegman, M. N., "Linear unification," <i>J. of Computer and System Sciences</i>, 16, 1978, 158--167.
• 11: {S} Sethi, R., cited in Garey and Johnson, p. 252.

INDEX TERMS

Primary Classification:
  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE

Additional Classification:
  I. Computing Methodologies
  I.1 SYMBOLIC AND ALGEBRAIC MANIPULATION

General Terms:
Theory