On the computational complexity of stratified negation in linear-time temporal logic programming

A lot of formal approaches to the "right" semantics of negation in logic programming have been proposed during the last two decades and the importance of this topic for the areas of Non-Monotonic Reasoning and Deductive Databases has been stressed. In sharp contrast, only a few papers have been devoted to the semantics of negation in temporal logic programming, despite the intuitive importance and the practical implication of this issue. Recently, a simple syntactic criterion has been proposed in la: it is based on the cycle sum test and singles out the Chronolog programs for which a well-defined semantics of stratified negation can be given. In this paper, we show that this test is computationally affordable, and thus of great practical importance too: we sketch an algorithm for the cycle sum test, whose time requirements are linearly related to the "size" of the input Chronolog program.