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: Franz Baader , Tobias Nipkow, Term rewriting and all that, Cambridge University Press, New York, NY, 1998
• 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: Hubert Comon , Pierre Lescanne, Equational problems and disunification, Journal of Symbolic Computation, v.7 n.3-4, p.371-425, March/April 1989 [doi>10.1016/S0747-7171(89)80017-3]
• 5: Hubert Comon , Ralf Treinen, Ordering Constraints on Trees, Proceedings of the 19th International Colloquium on Trees in Algebra and Programming, p.1-14, April 11-13, 1994
• 6: Hubert Comon , Ralf Treinen, The first-order theory of lexicographic path orderings is undecidable, Theoretical Computer Science, v.176 n.1-2, p.67-87, April 20, 1997 [doi>10.1016/S0304-3975(96)00049-7]
• 7: Dershowitz, N. 1982. Orderings for term rewriting systems. Theoret. Comput. Sci. 17, 279--301.
• 8: David Detlefs , Randy Forgaard, A Procedure for Automatically Proving the Termination of a Set of Rewrite Rules, Proceedings of the First International Conference on Rewriting Techniques and Applications, p.255-270, May 20-22, 1985
• 9: Jeremy Dick , John Kalmus , Ursula Martin, Automating the Knuth Bendix ordering, Acta Informatica, v.28 n.2, p.95-119, Dec. 1990 [doi>10.1007/BF01237233]
• 10: Harald Ganzinger , Robert Nieuwenhuis, Constraints and theorem proving, Constraints in computational logics: theory and applications, Springer-Verlag New York, Inc., New York, NY, 2001
• 11: Hodges, W. 1993. Model theory. Cambridge University Press, Cambridge, Mass.
• 12: Jean-Pierre Jouannaud , Mitsuhiro Okada, Satisfiability of systems of ordinal notations with the subterm property is decidable, Proceedings of the 18th international colloquium on Automata, languages and programming, p.455-468, June 1991, Madrid, Spain
• 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: Hélène Kirchner, On the Use of Constraints in Automated Deduction, Selected Papers from Constraint Programming: Basics and Trends, p.128-146, May 16-20, 1994
• 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: Konstantin Korovin , Andrei Voronkov, A Decision Procedure for the Existential Theory of Term Algebras with the Knuth-Bendix Ordering, Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science, p.291, June 26-29, 2000
• 17: Konstantin Korovin , Andrei Voronkov, Verifying Orientability of Rewrite Rules Using the Knuth-Bendix Order, Proceedings of the 12th International Conference on Rewriting Techniques and Applications, p.137-153, May 22-24, 2001
• 18: Konstantin Korovin , Andrei Voronkov, The Decidability of the First-Order Theory of the Knuth-Bendix Order in the Case of Unary Signatures, Proceedings of the 22nd Conference Kanpur on Foundations of Software Technology and Theoretical Computer Science, p.230-240, December 12-14, 2002
• 19: Konstantin Korovin , Andrei Voronkov, Orienting Equalities with the Knuth-Bendix Order, Proceedings of the 18th Annual IEEE Symposium on Logic in Computer Science, p.75, June 22-25, 2003
• 20: Konstantin Korovin , Andrei Voronkov, Orienting rewrite rules with the Knuth--Bendix order, Information and Computation, v.183 n.2, p.165-186, 15 June 2003 [doi>10.1016/S0890-5401(03)00021-X]
• 21: M. S. Krishnamoorthy , P. Narendran, On recursive path ordering, Theoretical Computer Science, v.40 n.2-3, p.323-328, Nov. 1985
• 22: Kenneth Kunen, Negation in logic programming, Journal of Logic Programming, v.4 n.4, p.289-308, December 1, 1987 [doi>10.1016/0743-1066(87)90007-0]
• 23: Lepper, I. 2001. Derivations lengths and order types of Knuth--Bendix orders. Theoret. Comput. Sci. 269, 1--2, 433--450.
• 24: Pierre Lescanne, Term Rewriting Systems and Algebra, Proceedings of the 7th International Conference on Automated Deduction, p.166-174, May 14-16, 1984
• 25: Bernd Löchner , Thomas Hillenbrand, A phytography of WALDMEISTER, AI Communications, v.15 n.2, p.127-133, September 2002
• 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: Ursula Martin, How to Choose Weights in the Knuth Bendix Ordering, Proceedings of the 2nd International Conference on Rewriting Techniques and Applications, p.42-53, May 25-27, 1987
• 29: Paliath Narendran , Michaël Rusinowitch, The Theory of Total Unary RPO Is Decidable, Proceedings of the First International Conference on Computational Logic, p.660-672, July 01, 2000
• 30: Paliath Narendran , Michaël Rusinowitch , Rakesh M. Verma, RPO Constraint Solving Is in NP, Proceedings of the 12th International Workshop on Computer Science Logic, p.385-398, August 24-28, 1998
• 31: Robert Nieuwenhuis, Simple LPO constraint solving methods, Information Processing Letters, v.47 n.2, p.65-69, Aug. 20, 1993 [doi>10.1016/0020-0190(93)90226-Y]
• 32: Robert Nieuwenhuis, Invited Talk: Rewrite-based Deduction and Symbolic Constraints, Proceedings of the 16th International Conference on Automated Deduction: Automated Deduction, p.302-313, July 07-10, 1999
• 33: Robert Nieuwenhuis , José Miguel Rivero, Solved Forms for Path Ordering Constraints, Proceedings of the 10th International Conference on Rewriting Techniques and Applications, p.1-15, July 02-04, 1999
• 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: Alexandre Riazanov , Andrei Voronkov, The design and implementation of VAMPIRE, AI Communications, v.15 n.2, p.91-110, September 2002
• 36: Stephan Schulz, E - a brainiac theorem prover, AI Communications, v.15 n.2, p.111-126, September 2002
• 37: K. N. Venkataraman, Decidability of the purely existential fragment of the theory of term algebras, Journal of the ACM (JACM), v.34 n.2, p.492-510, April 1987 [doi>10.1145/23005.24037]
• 38: Christoph Weidenbach, System Description: Spass Version 1.0.0, Proceedings of the 16th International Conference on Automated Deduction: Automated Deduction, p.378-382, July 07-10, 1999

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Computational logic

Additional Classification:
  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.3 Deduction and Theorem Proving
          Subjects: Resolution

General Terms:
Theory

Keywords:
Knuth--Bendix orders, Ordering constraints, automated deduction