×

Complexity of nilpotent unification and matching problems. (English) Zbl 1045.68603

Summary: We consider the complexity of equational unification and matching problems where the equational theory contains a nilpotent function, i.e., a function \(f\) satisfying \(f(x, x)=0\) where 0 is a constant. We show that nilpotent unification and matching are NP-complete. In the presence of associativity and commutativity, the problems still remain NP-complete. However, when 0 is also assumed to be the unity for the function \(f\), the problems are solvable in polynomial time. We also show that the problem remains in P even when a homomorphism is added. An application of this result to a subclass of set constraints is illustrated. Second-order matching modulo nilpotence is shown to be undecidable.

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
03B35 Mechanization of proofs and logical operations
68Q25 Analysis of algorithms and problem complexity
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Aiken, A., Set constraints: results, applications and future directions, Proceedings of the Second Workshop on Principles and Practice of Constraints Programming. Proceedings of the Second Workshop on Principles and Practice of Constraints Programming, Lecture Notes in Computer Science, 874 (1994), Springer-Verlag: Springer-Verlag Berlin, p. 326-335
[2] Aiken, A.; Kozen, D.; Vardi, M.; Wimmers, E., The complexity of set constraints, Proceedings of the 1993 Conference on Computer Science Logic. Proceedings of the 1993 Conference on Computer Science Logic, Lecture Notes in Computer Science, 832 (1993), Springer-Verlag: Springer-Verlag Berlin, p. 1-17 · Zbl 0953.68557
[3] Baader, F., Unification in commutative theories, Hilbert’s Basis Theorem, and Gröbner bases, J. Assoc. Comput. Mach., 40, 477-503 (1993) · Zbl 0791.68146
[4] Baader, F.; Schultz, K. U., Unification in the union of disjoint equational theories: combining decision procedures, Proceedings of the Eleventh Conference on Automated Deduction. Proceedings of the Eleventh Conference on Automated Deduction, Lecture Notes in Artificial Intelligence, 607 (1992), Springer-Verlag: Springer-Verlag Berlin, p. 50-65 · Zbl 0925.03084
[5] Baader, F.; Siekmann, J. S., Unification theory, (Gabbay, D. M.; Hogger, C. J.; Robinson, J. A., Handbook of Logic in Artificial Intelligence and Logic Programming (1994), Oxford University Press: Oxford University Press Oxford), 41-125
[6] Comon, H.; Haberstrau, M.; Jouannaud, J.-P., Decidable problems in shallow equational theories, Proceedings of the Seventh Annual IEEE Symposium on Logic in Computer Science (1992), IEEE Computer Society: IEEE Computer Society Washington, p. 255-265
[7] Dershowitz, N.; Jouannaud, J.-P., Rewrite systems, Handbook of Theoretical Computer Science (1990), Elsevier: Elsevier Amsterdam, p. 245-320 · Zbl 0900.68283
[8] Dershowitz, N.; Mitra, S.; Sivakumar, G., Decidable matching for convergent systems, Proceedings of the Eleventh Conference on Automated Deduction. Proceedings of the Eleventh Conference on Automated Deduction, Lecture Notes in Artificial Intelligence, 607 (1992), Springer-Verlag: Springer-Verlag Berlin, p. 589-602
[9] Garey, M. R.; Johnson, D. S., Computers and Intractability: A Guide to the Theory of NP-Completeness (1979), Freeman: Freeman San Francisco · Zbl 0411.68039
[10] Geddes, K. O.; Czapor, S. R.; Labahn, G., Algorithms for Computer Algebra (1992), Kluwer Academic: Kluwer Academic Boston · Zbl 0805.68072
[11] Goldfarb, W. D., The undecidability of the second-order unification problem, Theoret. Comput. Sci., 13, 225-230 (1981) · Zbl 0457.03006
[12] Heintze, N., Set-based analysis of ML programs, Proceedings of the 1994 ACM Conference on Lisp and Functional Programming (1994), p. 306-317
[13] Hermann, M.; Kolaitis, P. G., Unification algorithms cannot be combined in polynomial time, Proceedings of the Thirteenth Conference on Automated Deduction. Proceedings of the Thirteenth Conference on Automated Deduction, Lecture Notes in Artificial Intelligence, 1104 (1996), Springer-Verlag: Springer-Verlag Berlin, p. 246-260 · Zbl 1412.68233
[14] Hullot, J.-M., Canonical forms and unification, Proceedings of the Fifth Conference on Automated Deduction. Proceedings of the Fifth Conference on Automated Deduction, Lecture Notes in Computer Science, 87 (1980), Springer-Verlag: Springer-Verlag Berlin, p. 318-334
[15] Jouannaud, J.-P.; Kirchner, C., Solving equations in abstract algebras: a rule-based survey of unification, Computational Logic: Essays in Honor of Alan Robinson (1991), MIT Press: MIT Press Boston, p. 360-394
[16] Kaltofen, E.; Krishnamoorthy, M. S.; Saunders, B. D., Fast parallel computation of Hermite and Smith forms of polynomial matrices, SIAM J. Algebraic Discrete Methods, 8, 683-690 (1987) · Zbl 0655.65069
[17] Kapur, D.; Narendran, P., NP-completeness of the set unification and matching problems, Proceedings of the Eighth Conference on Automated Deduction. Proceedings of the Eighth Conference on Automated Deduction, Lecture Notes in Computer Science, 230 (1986), Springer-Verlag: Springer-Verlag Berlin, p. 489-495
[18] Kapur, D.; Narendran, P., Complexity of unification problems with associative-commutative operators, J. Automated Reason., 9, 261-280 (1992) · Zbl 0781.68076
[19] Kirchner, C., Computing unification algorithms, Proceedings of the First Annual IEEE Symposium on Logic in Computer Science (1986), IEEE Computer Society: IEEE Computer Society Washington, p. 206-216
[20] Martelli, A.; Montanari, U., An efficient unification algorithm, ACM Trans. Progr. Languages Systems, 4, 258-282 (1982) · Zbl 0478.68093
[21] Narendran, P.; Pfenning, F.; Statman, R., On the unification problem for cartesian closed categories, Proceedings of the Eighth Annual IEEE Symposium on Logic in Computer Science (1993), IEEE Computer Society: IEEE Computer Society Washington, p. 57-63
[22] Nutt, W., Unification in monoidal theories, Proceedings of the 10th International Conference on Automated Deduction. Proceedings of the 10th International Conference on Automated Deduction, Lecture Notes in Computer Science, 449 (1990), Springer-Verlag: Springer-Verlag Berlin, p. 618-632 · Zbl 1509.03045
[23] Plotkin, G. D., Building-in equational theories, Machine Intelligence (1972), p. 73-90 · Zbl 0262.68036
[24] Schaefer, T. J., The complexity of satisfiability problems, Proceedings of the Tenth Annual ACM Symposium on Theory of Computing (1978), p. 216-226 · Zbl 1282.68143
[25] Schmidt-Schauss, M., An Algorithm for Distributive Unification (1995), Universität FrankfurtFachbereich Informatik: Universität FrankfurtFachbereich Informatik Frankfurt · Zbl 1503.03020
[26] Wolfram, D. A., The Clausal Theory of Types (1993), Cambridge Univ. Press: Cambridge Univ. Press Cambridge · Zbl 0782.68007
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.