Knuth-Bendix Constraint Solving Is NP-Complete

1. F. Baader and T. Nipkow. Term Rewriting and and All That. Cambridge University press, Cambridge, 1998.

   Google Scholar 

2. H. Comon. Solving symbolic ordering constraints. International Journal of Foundations of Computer Science, 1(4):387–411, 1990.

   Article  MATH  MathSciNet  Google Scholar 

3. N. Dershowitz. Orderings for term rewriting systems. Theoretical Computer Science, 17:279–301, 1982.

   Article  MATH  MathSciNet  Google Scholar 

4. Th. Hillenbrand, A. Buch, R. Vogt, and B. Löchner. Waldmeister: High-performance equational deduction. Journal of Automated Reasoning, 18(2):265–270, 1997.

   Article  Google Scholar 

5. W. Hodges. Model theory. Cambridge University Press, 1993.

   Google Scholar 

6. J.-P. Jouannaud and M. Okada. Satisfiability of systems of ordinal notations with the subterm property is decidable. In J.L. Albert, B. Monien, and M. Rodróguez-Artalejo, editors, Automata, Languages and Programming, 18th International Colloquium, ICALP’91, volume 510 of Lecture Notes in Computer Science, pages 455–468, Madrid, Spain, 1991. Springer Verlag.

   Google Scholar 

7. H. Kirchner. On the use of constraints in automated deduction. In A. Podelski, editor, Constraint Programming: Basics and Tools, volume 910 of Lecture Notes in Computer Science, pages 128–146. Springer Verlag, 1995.

   Google Scholar 

8. D. Knuth and P. Bendix. Simple word problems in universal algebras. In J. Leech, editor, Computational Problems in Abstract Algebra, pages 263–297. Pergamon Press, Oxford, 1970.

   Google Scholar 

9. K. Korovin and A. Voronkov. A decision procedure for the existential theory of term algebras with the Knuth-Bendix ordering. In Proc. 15th Annual IEEE Symp. on Logic in Computer Science, pages 291–302, Santa Barbara, California, June 2000.

   Google Scholar 

10. K. Korovin and A. Voronkov. Knuth-Bendix constraint solving is NP-complete. Preprint CSPP-8, Department of Computer Science, University of Manchester, February 2000.

    Google Scholar 

11. P. Narendran, M. Rusinowitch, and R. Verma. RPO constraint solving is in NP. In G. Gottlob, E. Grandjean, and K. Seyr, editors, Computer Science Logic, 12th International Workshop, CSL’98, volume 1584 of Lecture Notes in Computer Science, pages 385–398. Springer Verlag, 1999.

    Google Scholar 

12. R. Nieuwenhuis. Simple LPO constraint solving methods. Information Processing Letters, 47:65–69, 1993.

    Article  MATH  MathSciNet  Google Scholar 

13. R. Nieuwenhuis. Rewrite-based deduction and symbolic constraints. In H. Ganzinger, editor, Automated Deduction—CADE-16. 16th International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence, pages 302–313, Trento, Italy, July 1999.

    Google Scholar 

14. A. Riazanov and A. Voronkov. Vampire. In H. Ganzinger, editor, Automated Deduction—CADE-16. 16th International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence, pages 292–296, Trento, Italy, July 1999.

    Google Scholar 

15. S. Schulz. System abstract: E 0.3. In H. Ganzinger, editor, Automated Deduction— CADE-16. 16th International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence, pages 297–301, Trento, Italy, July 1999.

    Google Scholar 

16. C. Weidenbach, B. Afshordel, U. Brahm, C. Cohrs, T. Engel, E. Keen, C. Theobalt, and D. Topic. System description: Spass version 1.0.0. In H. Ganzinger, editor, Automated Deduction—CADE-16. 16th International Conference on Automated Deduction, volume 1632 of Lecture Notes in Artificial Intelligence, pages 378–382, Trento, Italy, July 1999.

    Google Scholar 

Download references