Database Entry Point
max planck institut
mpii logo Minerva of the Max Planck Society

Publications Master Template, generated: 0:20, 17 October 2019

Search the publication database

  . Return

Your search returned the following 10 documents:

  1. Konstantin Korovin and Andrei Voronkov
    Knuth-Bendix constraint solving is NP-complete
    ACM Transactions on Computational Logic 6 (2): 361-388, 2005
  2. Konstantin Korovin and Andrei Voronkov
    Orienting Equalities with the Knuth-Bendix Order
    In: 18th Annual IEEE Symposium on Logic in Computer Science (LICS-03), Ottawa, Canada, June, 22 - June, 25, 2003, 75-84

  3. Konstantin Korovin and Andrei Voronkov
    Orienting rewrite rules with the Knuth-Bendix order
    Information and Computation 183 (2): 165-186, 2003
  4. Konstantin Korovin and Andrei Voronkov
    AC-compatible Knuth-Bendix Order
    In: Automated deduction, CADE-19 : 19th International Conference on Automated Deduction, Miami, Florida, July, 30 - August, 2, 2003, 47-59

  5. Robert Nieuwenhuis, Thomas Hillenbrand, Alexandre Riazanov, and Andrei Voronkov
    On the Evaluation of Indexing Techniques for Theorem Proving
    In: Automated reasoning : First International Joint Conference, IJCAR 2001, Siena, Italy, June, 18-22, 2001, 257-271
    [PS: Download:]
  6. Anatoli Degtyarev, Yuri Gurevich, Paliath Narendran, Margus Veanes, and Andrei Voronkov
    Decidability and Complexity of Simultaneous Rigid E-unification with One Variable and Related Results
    Theoretical Computer Science 243 (1/2): 167-184, 2000
  7. Andrei Voronkov
    The ground-negative fragment of first-order logics is $\pi^p_2$-complete
    The Journal of Symbolic Logic 64 (3): 984-990, 1999
  8. Sergei Vorobyov and Andrei Voronkov
    Complexity of Nonrecursive Logic Programs with Complex Values
    In: Proceedings of the 17th ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems (PODS-98), Saeattle, Washington, U.S.A., June 1-4, 1998, 1998, 244-253

  9. Leo Bachmair, Harald Ganzinger, and Andrei Voronkov
    Elimination of Equality via Transformation with Ordering Constraints
    In: Proceedings of the 15th International Conference on Automated Deduction (CADE-98), Lindau, Germany, July, 5-10 1998, 1998, 175-190. Note: Short version of MPI-I-97-2-012
  10. Anatoli Degtyarev, Yuri Gurevich, Paliath Narendran, Margus Veanes, and Andrei Voronkov
    The Decidability of Simultaneous Rigid E-Unification with One Variable
    In: Proceedings of the 9th International Conference on Rewriting Techniques and Applications (RTA-98), Tsukuba, Japan, March 30 - April 1, 1998, 1998, 181-195