Knuth-Bendix constraint solving is NP-complete

Konstantin Korovin; Andrei Voronkov

doi:10.1145/1055686.1055692

Knuth-Bendix constraint solving is NP-complete

Research output: Contribution to journal › Article

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 language	English
Pages (from-to)	361-388
Number of pages	27
Journal	ACM Transactions on Computational Logic
Volume	6
Issue number	2
DOIs	https://doi.org/10.1145/1055686.1055692
Publication status	Published - Apr 2005

Keywords

Automated deduction
Knuth-Bendix orders
Ordering constraints

Access to Document

10.1145/1055686.1055692

Cite this

@article{0d341b222bd74f08a40889a9d9f5fe49,

title = "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. {\textcopyright} 2005 ACM.",

keywords = "Automated deduction, Knuth-Bendix orders, Ordering constraints",

author = "Konstantin Korovin and Andrei Voronkov",

note = "informal publication",

year = "2005",

month = apr,

doi = "10.1145/1055686.1055692",

language = "English",

volume = "6",

pages = "361--388",

journal = "ACM Transactions on Computational Logic",

issn = "1529-3785",

publisher = "Association for Computing Machinery",

number = "2",

}

TY - JOUR

T1 - Knuth-Bendix constraint solving is NP-complete

AU - Korovin, Konstantin

AU - Voronkov, Andrei

N1 - informal publication

PY - 2005/4

Y1 - 2005/4

N2 - 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.

AB - 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.

KW - Automated deduction

KW - Knuth-Bendix orders

KW - Ordering constraints

U2 - 10.1145/1055686.1055692

DO - 10.1145/1055686.1055692

M3 - Article

SN - 1529-3785

VL - 6

SP - 361

EP - 388

JO - ACM Transactions on Computational Logic

JF - ACM Transactions on Computational Logic

IS - 2

ER -

Knuth-Bendix constraint solving is NP-complete

Abstract

Keywords

Access to Document

Fingerprint

Cite this