Temporal constraint satisfaction problems in least fixed point logic
From International Center for Computational Logic
Temporal constraint satisfaction problems in least fixed point logic
Talk by Jakub Rydval
- Location: APB 3027
- Start: 1. November 2018 at 1:00 pm
- End: 1. November 2018 at 2:30 pm
- Research group: Automata Theory
- Event series: KBS Seminar
- iCal
The constraint satisfaction problem (CSP) for a fixed structure L with finite relational signature is the computational problem of deciding whether a given finite structure of the same signature homomorphically maps to L. A temporal constraint language is a structure over the rational numbers Q whose relations are first-order definable in (Q;<). In 2009, Bodirsky and Kara presented a complete classification of the computational complexity of CSPs for temporal constraint languages. In contrast to finite domain structures, there are temporal constraint languages whose CSP cannot be solved by any Datalog program but can be expressed in least fixed point logic (LFP). An example is CSP(Q; { (x,y,z), where x>y or x>z} ), known as the and/or scheduling problem. I will give a proof of a dichotomy for LFP expressibility of CSPs of temporal constraint languages. For a temporal constraint language L, exactly one of the following is true: either L interprets all finite structures primitively positively with parameters and CSP(L) is inexpressible in LFP, or CSP(L) is inexpressible in LFP if and only if L admits a primitive positive definition of the relation X:={ (x,y,z), where x>y=z or y>z=x or z>x=y}.
