Name
Abstract | ||
|---|---|---|
The CSP of a first-order theory T is the problem of deciding for a given finite set S of atomic formulas whether T. S is satisfiable. Let T-1 and T-2 be two theories with countably infinite models and disjoint signatures. Nelson and Oppen presented conditions that imply decidability (or polynomial-time decidability) of CSP(T-1 boolean OR T-2) under the assumption that CSP(T-1) and CSP(T-2) are decidable (or polynomial-time decidable). We show that for a large class of - categorical theories T-1, T-2 the Nelson-Oppen conditions are not only sufficient, but also necessary for polynomial-time tractability of CSP(T-1 boolean OR T-2) (unless P = NP). |
Year | DOI | Venue |
|---|---|---|
2018 | 10.1007/978-3-319-94205-6_18 | Lecture Notes in Artificial Intelligence |
DocType | Volume | ISSN |
Conference | 10900 | 0302-9743 |
Citations | PageRank | References |
0 | 0.34 | 22 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Manuel Bodirsky | 1 | 644 | 54.63 |
| Johannes Greiner | 2 | 0 | 0.68 |