We introduce negation under the stable model semantics in DatalogMTL - a temporal extension of Datalog with metric temporal operators. As a result, we obtain a rule language which combines the power of answer set programming with the temporal dimension provided by metric operators. We show that, in this setting, reasoning becomes undecidable over the rational timeline, and decidable in EXPSPACE in data complexity over the integer timeline. We also show that, if we restrict our attention to forward-propagating programs, reasoning over the integer timeline becomes PSPACE-complete in data complexity, and hence, no harder than over positive programs; however, reasoning over the rational timeline in this fragment remains undecidable. Under consideration in Theory and Practice of Logic Programming (TPLP).
翻译:我们在DatalogMTL中引入了带稳定模型语义的否定——DatalogMTL是Datalog在度量时间算子上的时间扩展。由此,我们获得了一种结合了回答集编程能力与度量算子提供的时间维度的规则语言。我们证明,在此设定下,在有理数时间线上推理变得不可判定,而在整数时间线上数据复杂度为EXPSPACE时可判定。我们还证明,若将注意力限制于前向传播程序,在整数时间线上数据复杂度为PSPACE完全时推理仍可判定,因此不比正程序更困难;然而,在该片段中对有理数时间线的推理仍然不可判定。本文正在《逻辑编程理论与实践》(TPLP)期刊评审中。