Abstract | ||
---|---|---|
Finite-domain constraint satisfaction problems are either solvable by Datalog, or not even expressible in fixed-point logic with counting. The border between the two regimes can be described by a strong height-one Maltsev condition. For infinite-domain CSPs, the situation is more complicated even if the template structure of the CSP is model-theoretically tame. We prove that there is no Maltsev condition that characterizes Datalog already for the CSPs of first-order reducts of (Q; <); such CSPs are called temporal CSPs and are of fundamental importance in infinite-domain constraint satisfaction. Our main result is a complete classification of temporal CSPs that can be expressed in one of the following logical formalisms: Datalog, fixed-point logic (with or without counting), or fixed-point logic with the Boolean rank operator. The classification shows that many of the equivalent conditions in the finite fail to capture expressibility in Datalog or fixed-point logic already for temporal CSPs.
|
Year | DOI | Venue |
---|---|---|
2020 | 10.1145/3373718.3394750 | LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science
Saarbrücken
Germany
July, 2020 |
Keywords | DocType | ISSN |
temporal constraint satisfaction problems, fixed-point logic, Maltsev conditions | Conference | 1043-6871 |
ISBN | Citations | PageRank |
978-1-4503-7104-9 | 0 | 0.34 |
References | Authors | |
0 | 3 |
Name | Order | Citations | PageRank |
---|---|---|---|
Manuel Bodirsky | 1 | 644 | 54.63 |
Wied Pakusa | 2 | 11 | 4.18 |
Rydval Jakub | 3 | 0 | 0.34 |