In this note we consider the problem of introducing variables in temporal logic programs under the formalism of "Temporal Equilibrium Logic" (TEL), an extension of Answer Set Programming (ASP) for dealing with linear-time modal operators. To this aim, we provide a definition of a first-order version of TEL that shares the syntax of first-order Linear-time Temporal Logic (LTL) but has a different semantics, selecting some LTL models we call "temporal stable models". Then, we consider a subclass of theories (called "splittable temporal logic programs") that are close to usual logic programs but allowing a restricted use of temporal operators. In this setting, we provide a syntactic definition of "safe variables" that suffices to show the property of "domain independence" -- that is, addition of arbitrary elements in the universe does not vary the set of temporal stable models. Finally, we present a method for computing the derivable facts by constructing a non-temporal logic program with variables that is fed to a standard ASP grounder. The information provided by the grounder is then used to generate a subset of ground temporal rules which is equivalent to (and generally smaller than) the full program instantiation.

本研究介绍了“时间平衡逻辑”（TEL）的第一阶段版本，它与一阶线性时间逻辑（LTL）共享语法但具有不同的语义，选择了一些我们称之为“时间稳定模型”的LTL模型，并提出了计算可推导事实的方法。

带变量的时间逻辑程序