Knuth-Bendix constraint solving is NP-complete

Konstantin Korovin, Andrei Voronkov

    Research output: Contribution to journalArticle

    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. © 2005 ACM.
    Original languageEnglish
    Pages (from-to)361-388
    Number of pages27
    JournalACM Transactions on Computational Logic
    Volume6
    Issue number2
    DOIs
    Publication statusPublished - Apr 2005

    Keywords

    • Automated deduction
    • Knuth-Bendix orders
    • Ordering constraints

    Fingerprint

    Dive into the research topics of 'Knuth-Bendix constraint solving is NP-complete'. Together they form a unique fingerprint.

    Cite this