Abstract
All applications of equational unification in the area of term rewriting and theorem proving require algorithms for general E-unification, i.e., E-unification with free function symbols. On this background, the complexity of general E-unification algorithms has been investigated for a large number of equational theories. For most of the relevant cases, the problem of deciding solvability of general E-unification problems was found to be NP-hard. We offer a partial explanation. A criterion is given that characterizes a large class K of equational theories E where general E-unification is always NP-hard. We show that all regular equational theories E that contain a commutative or an associative function symbol belong to K. Other examples of equational theories in K concern non-regular cases as well.
The combination algorithm described in [BS92] can be used to reduce solvability of general E-unification algorithms to solvability of E- and free (Robinson) unification problems with linear constant restrictions. We show that for E ∈ K there exists no polynomial optimization of this combination algorithm for deciding solvability of general E-unification problems, unless P=NP. This supports the conjecture that for E ∈ K there is no polynomial algorithm for combining E-unification with constants with free unification.
This work was supported by the EC Working Group CCL, EP6028.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
F. Baader, K.U. Schulz, “Unification in the union of disjoint equational theories: Combining decision procedures,” in: Proc. CADE-11, LNAI 607, 1992, pp. 50–65.
F. Baader, K.U. Schulz, “Unification in the union of disjoint equational theories: Combining decision procedures,” Journal of Symbolic Computation, 21 (1996), pp. 211–243.
F. Baader, J. Siekmann, “Unification Theory,” in D.M. Gabbay, C. Hogger, and J. Robinson, Editors, Handbook of Logic in Artificial Intelligence and Logic Programming, Oxford University Press, Oxford, UK, 1994, pp. 41–125.
L. Bachmair, Canonical equational proofs, Progress in Theoretical Computer Science, Birkhäuser, Boston, 1991.
A. Boudet, “Combining Unification Algorithms,” Journal of Symbolic Computation 16 (1993) pp. 597–626.
M.R. Garey, D.S. Johnson, “Computers and Intractability: A Guide to the Theory of NP-Completeness,” W.H. Freeman and Co. San Francisco (1979).
Q. Guo, P. Narendran, and D.A. Wolfram “Unification and Matching modulo Nilpotence,” manuscript, received from Qing Guo, guo@cs.albany.edu, 1996.
M. Hermann, P.G. Kolaitis, “Unification Algorithms Cannot be Combined in Polynomial Time,” in Proceedings of the 13th International Conference on Automated Deduction, M.A. McRobbie and J.K. Slaney (Eds.), Springer LNAI 1104, 1996, pp. 246–260.
A. Herold, “Combination of Unification Algorithms,” Proceedings of the 8th International Conference on Automated Deduction, LNCS 230, 1986, pp. 450–469.
J.P. Jouannaud, H. Kirchner, “Completion of a set of rules modulo a set of equations.” SIAM J. Computing 15, 1986, pp. 1155–1194.
D. Kapur, P. Narendran, “Complexity of Unification Problems with Associative-Commutative Operators,” J. Automated Reasoning 9, 1992, pp. 261–288.
S. Kepser, J. Richts, “Optimization Techniques for the Combination of Unification Algorithms,” to be submitted.
C. Kirchner, “Méthodes et outils de conception systématique d'algorithmes d'unification dans les théories équationelles,” Thèse d'Etat, Université de Nancy 1, France, 1985.
R. Niewenhuis, A. Rubio, “AC-superposition with constraints: No AC-unifiers needed,” in Proceedings of the 12th International Conference on Automated Deduction, Nancy, France, A. Bundy (Ed.), Springer LNAI 1994, pp.545–559.
G. Plotkin, “Building in equational theories,” Machine Intelligence 7, 1972, pp. 73–90.
A. Rubio, “Theorem Proving modulo Associativity,” in Proceedings Computer Science Logic CSL'95, Paderborn, Germany, H. Kleine Büning (Ed.), Springer LNCS 1092 (1995), pp. 452–467.
M. Schmidt-Schauß, “Combination of Unification Algorithms,” J. Symbolic Computation 8, 1989, pp. 51–99.
K.U. Schulz, “Combination of Unification and Disunification Algorithms: Tractable and Intractable Instances,” Research Paper, available under ftp.cis.uni-muenchen.de, in directory pub/schulz. File name: ComplexityCombination.ps.gz
M. Stickel, “Automated deduction by theory resolution,” J. Automated Reasoning 1, 1985, pp. 333–356.
E. Tiden, “Unification in Combinations of Collapse Free Theories with Disjoint Sets of Function Symbols,” Proceedings of the 8th International Conference on Automated Deduction, LNCS 230, 1986.
K. Yelick, “Unification in Combinations of Collapse Free Regular Theories,” J. Symbolic Computation 3, 1987.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Schulz, K.U. (1997). A criterion for intractability of E-unification with free function symbols and its relevance for combination of unification algorithms. In: Comon, H. (eds) Rewriting Techniques and Applications. RTA 1997. Lecture Notes in Computer Science, vol 1232. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-62950-5_78
Download citation
DOI: https://doi.org/10.1007/3-540-62950-5_78
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-62950-4
Online ISBN: 978-3-540-69051-1
eBook Packages: Springer Book Archive