A Fast Algorithm and Datalog Inexpressibility for Temporal Reasoning
Manuel Bodirsky, Jan Kara
TL;DR
This paper presents a new efficient algorithm for a broad temporal constraint language and proves its inexpressibility in Datalog, highlighting limitations of existing logical frameworks for temporal reasoning.
Contribution
It introduces a tractable temporal constraint language extending previous classes and provides a quadratic-time decision algorithm, along with a proof of Datalog inexpressibility.
Findings
Quadratic-time algorithm for the new temporal language
The language strictly contains Ord-Horn and AND/OR precedence constraints
Proven inexpressibility in Datalog and local consistency methods
Abstract
We introduce a new tractable temporal constraint language, which strictly contains the Ord-Horn language of Buerkert and Nebel and the class of AND/OR precedence constraints. The algorithm we present for this language decides whether a given set of constraints is consistent in time that is quadratic in the input size. We also prove that (unlike Ord-Horn) this language cannot be solved by Datalog or by establishing local consistency.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsConstraint Satisfaction and Optimization · Logic, Reasoning, and Knowledge · Model-Driven Software Engineering Techniques