Abstract
The set-unification and set-matching problems, which are very restricted cases of the associative-commutative-idempotent unification and matching problems, respectively, are shown to be NP-complete. The NP-completeness of the subsumption check in first-order resolution follows from these results. It is also shown that commutative-idempotent matching and associative-idempotent matching are NP-hard, thus implying that the idempotency of a function does not help in reducing the complexity of matching and unification problems.
Partially supported by the National Science Foundation Grant no. DCR-8408461.
Preview
Unable to display preview. Download preview PDF.
6. References
Benanav, D., Kapur, D., and Narendran, P., ”Complexity of Matching Problems,” Proc. of the First International Conf on Rewrite Techniques and Applications, Dijon, France, May 1985.
Chang, C.-L., and Lee, R. C.-T., Symbolic Logic and Mechanical Theorem Proving. Academic Press, New York, 1973.
Garey, M.R., and Johnson, D.S., Computers and Intractability, W.H. Freeman, 1979.
Hsiang, J., ”Refutational Theorem Proving Using Term Rewriting Systems,” Artificial Intelligence 25 (3), pp. 255–300, March 1985.
Kapur, D., and Narendran, P., ”An Equational Approach to Theorem Proving in First-Order Predicate Calculus,” Proc. of the Ninth International Joint Conf. on Artificial Intelligence, Los Angeles, August 1985.
Paterson, M.S., and Wegman, M., ”Linear Unification,” Journal of Computer and System Sciences 16, pp. 158–167, 1978.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1986 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kapur, D., Narendran, P. (1986). NP-completeness of the set unification and matching problems. In: Siekmann, J.H. (eds) 8th International Conference on Automated Deduction. CADE 1986. Lecture Notes in Computer Science, vol 230. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-16780-3_113
Download citation
DOI: https://doi.org/10.1007/3-540-16780-3_113
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-16780-8
Online ISBN: 978-3-540-39861-5
eBook Packages: Springer Book Archive