Temporal constraint satisfaction problems in least fixed point logic
Aus International Center for Computational Logic
Temporal constraint satisfaction problems in least fixed point logic
Vortrag von Jakub Rydval
- Veranstaltungsort: APB 3027
- Beginn: 1. November 2018 um 13:00
- Ende: 1. November 2018 um 14:30
- Forschungsgruppe: Automatentheorie
- 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}.
