Temporal Logic Programs with Variables

TL;DR

This paper extends Answer Set Programming with temporal logic and variables, defining a first-order TEL, identifying safe variables for domain independence, and proposing a practical grounding method.

Contribution

It introduces a first-order version of TEL, defines safe variables for domain independence, and presents a method for efficient grounding using standard ASP tools.

Findings

Defined first-order TEL with temporal stable models.

Identified safe variables ensuring domain independence.

Proposed a grounding method reducing program size.

Abstract

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.