Knuth--bendix constraint solving is NP-complete

Abstract

We show the NP-completeness of the existential theory of term algebras with the Knuth--Bendix order by giving a nondeterministic polynomial-time algorithm for solving Knuth--Bendix ordering constraints.

References

1. Baader, F. and Nipkow, T. 1998. Term Rewriting and All That. Cambridge University Press, Cambridge, mass.]]
2. Belegradek, O. 1988. Model theory of locally free algebras (in Russian). In Model Theory and its Applications. Trudy Instituta Matematiki, vol. 8. Nauka, Novosibirsk, 3--24. (English translation in Translations of the American Mathematical Society.)]]
3. Comon, H. 1990. Solving symbolic ordering constraints. Int. J. Found. Comput. Sci. 1, 4, 387--411.]]
4. Comon, H. and Lescanne, P. 1989. Equational problems and disunification. Journal of Symbolic Computations 7, 3, 4, 371--425.]]
5. Comon, H. and Treinen, R. 1994. Ordering constraints on trees. In Trees in Algebra and Programming: CAAP'94, S. Tison, Ed. Lecture Notes in Computer Science, vol. 787. Springer-Verlag, New York, 1--14.]]
6. Comon, H. and Treinen, R. 1997. The first-order theory of lexicographic path orderings is undecidable. Theoret. Comput. Sci. 176, 1--2, 67--87.]]
7. Dershowitz, N. 1982. Orderings for term rewriting systems. Theoret. Comput. Sci. 17, 279--301.]]
8. Detlefs, D. and Forgaard, R. 1985. A procedure for automatically proving the termination of a set of rewrite rules. In Rewriting Techniques and Applications, First International Conference, RTA-85 (Dijon, France), J.-P. Jouannaud, Ed. Lecture Notes in Computer Science, vol. 202. Springer-Verlag, New York, 255--270.]]
9. Dick, J., Kalmus, J., and Martin, U. 1990. Automating the Knuth--Bendix ordering. Acta Inf. 28, 2, 95--119.]]
10. Ganzinger, H. and Nieuwenhuis, R. 2001. Constraints and theorem proving. In Constraints in Computational Logics, International Summer School, September 5--8, 1999, Gif-sur-Yvette, France, Edition, H. Comon, C. Marché, and R. Treinen, Eds. Lecture Notes in Computer Science, vol. 2002. Springer-Verlag, New York, 159--201.]]
11. Hodges, W. 1993. Model theory. Cambridge University Press, Cambridge, Mass.]]
12. Jouannaud, J.-P. and Okada, M. 1991. Satisfiability of systems of ordinal notations with the subterm property is decidable. In Automata, Languages and Programming, 18th International Colloquium, ICALP'91 (Madrid, Spain), J. Albert, B. Monien, and M. Rodríguez-Artalejo, Eds. Lecture Notes in Computer Science, vol. 510. Springer-Verlag, New York, 455--468.]]
13. Kamin, S. and Lévy, J.-J. 1980. Attempts for generalizing the recursive path orderings. Unpublished manuscript. (Available on the Web page of Pierre Lescanne: http.//perso.ens-lyon.fr/pierre.lescanne/not accessible.html.)]]
14. Kirchner, H. 1995. On the use of constraints in automated deduction. In Constraint Programming: Basics and Tools, A. Podelski, Ed. Lecture Notes in Computer Science, vol. 910. Springer-Verlag, New York, 128--146.]]
15. Knuth, D. and Bendix, P. 1970. Simple word problems in universal algebras. In Computational Problems in Abstract Algebra, J. Leech, Ed. Pergamon Press, Oxford, 263--297.]]
16. Korovin, K. and Voronkov, A. 2000. A decision procedure for the existential theory of term algebras with the Knuth--Bendix ordering. In Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science, (LICS'00). IEEE Computer Society Press, Los Alamitos, California, 291--302.]]
17. Korovin, K. and Voronkov, A. 2001. Verifying orientability of rewrite rules using the Knuth--Bendix order. In Rewriting Techniques and Applications, 12th International Conference, RTA 2001, A. Middeldorp, Ed. Lecture Notes in Computer Science, vol. 2051. Springer-Verlag, New York, 137--153. (Journal version: {Korovin and Voronkov 2003b}.)]]
18. Korovin, K. and Voronkov, A. 2002. The decidability of the first-order theory of the Knuth--Bendix order in the case of unary signatures. In Proceedings of the 22th Conference on Foundations of Software Technology and Theoretical Computer Science, (FSTTCS'02). Lecture Notes in Computer Science, vol. 2556. Springer-Verlag, New York, 230--240.]]
19. Korovin, K. and Voronkov, A. 2003a. Orienting equalities with the Knuth--Bendix order. In Proceedings of the 18th IEEE Symposium on Logic in Computer Science, (LICS'03). IEEE Computer Society Press, Los Alamitos, Calif., 75--84.]]
20. Korovin, K. and Voronkov, A. 2003b. Orienting rewrite rules with the Knuth--Bendix order. Inf. Comput. 183, 2, 165--186.]]
21. Krishnamoorthy, M. and Narendran, P. 1985. On recursive path ordering. Theoret. Comput. Sci. 40, 323--328.]]
22. Kunen, K. 1987. Negation in logic programming. J. Logic Prog. 4, 289--308.]]
23. Lepper, I. 2001. Derivations lengths and order types of Knuth--Bendix orders. Theoret. Comput. Sci. 269, 1--2, 433--450.]]
24. Lescanne, P. 1984. Term rewriting systems and algebra. In Proceedings of the 7th International Conference on Automated Deduction, CADE-7, R. Shostak, Ed. Lecture Notes in Computer Science, vol. 170. Springer Verlag, New York, 166--174.]]
25. Löchner, B. and Hillenbrand, T. 2002. A phytography of WALDMEISTER. AI Commun. 15, 2--3, 127--133.]]
26. Maher, M. 1988. Complete axiomatizations of the algebras of finite, rational and infinite trees. In Proceedings of the IEEE Conference on Logic in Computer Science (LICS). IEEE Computer Society Press, Los Alamitos, Calif., 348--357.]]
27. Maĺcev, A. 1961. On the elementary theories of locally free universal algebras. Soviet Math. Dokl. 2, 3, 768--771.]]
28. Martin, U. 1987. How to choose weights in the Knuth--Bendix ordering. In Rewriting Technics and Applications. Lecture Notes in Computer Science, vol. 256. Springer-Verlag, New York, 42--53.]]
29. Narendran, P. and Rusinowitch, M. 2000. The theory of total unary RPO is decidable. In Proceedings of 1st International Conference on Computational Logic, CL'2000. Lecture Notes in Computer Science, vol. 1861. Springer-Verlag, New York, 660--672.]]
30. Narendran, P., Rusinowitch, M., and Verma, R. 1999. RPO constraint solving is in NP. In Computer Science Logic, 12th International Workshop, CSL'98, G. Gottlob, E. Grandjean, and K. Seyr, Eds. Lecture Notes in Computer Science, vol. 1584. Springer-Verlag, New York, 385--398.]]
31. Nieuwenhuis, R. 1993. Simple LPO constraint solving methods. Inf. Proc. Lett. 47, 65--69.]]
32. Nieuwenhuis, R. 1999. Rewrite-based deduction and symbolic constraints. In Automated Deduction---CADE-16, 16th International Conference on Automated Deduction (Trento, Italy). H. Ganzinger, Ed. Lecture Notes in Artificial Intelligence, vol. 1632. Springer-Verlag, New York, 302--313.]]
33. Nieuwenhuis, R. and Rivero, J. 1999. Solved forms for path ordering constraints. In Proceedings of the 10th International Conference on Rewriting Techniques and Applications (RTA) (Trento, Italy). Lecture Notes in Computer Science, vol. 1631. Springer-Verlag, New York, 1--15.]]
34. Nieuwenhuis, R. and Rubio, A. 2001. Paramodulation--based theorem proving. In Handbook of Automated Reasoning, A. Robinson and A. Voronkov, Eds. Vol. I. Elsevier Science, Amsterdam, The Netherlands, Chap. 7, 371--443.]]
35. Riazanov, A. and Voronkov, A. 2002. The design and implementation of Vampire. AI Commun. 15, 2--3, 91--110.]]
36. Schulz, S. 2002. E---A brainiac theorem prover. AI Commun. 15, 2--3, 111--126.]]
37. Venkataraman, K. N. 1987. Decidability of the purely existential fragment of the theory of term algebras. J. ACM 34, 2, 492--510.]]
38. Weidenbach, C., Afshordel, B., Brahm, U., Cohrs, C., Engel, T., Keen, E., Theobalt, C., and Topic, D. 1999. System description: SPASS version 1.0.0. In Automated Deduction---CADE-16, 16th International Conference on Automated Deduction (Trento, Italy). H. Ganzinger, Ed. Lecture Notes in Artificial Intelligence, vol. 1632. Springer-Verlag, New York, 378--382.]]

Index Terms

• Computing methodologies

  • Artificial intelligence

    • Knowledge representation and reasoning

• Theory of computation

  • Logic