Temporal Logic Programs with Variables
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.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Towards Tighter Convex Relaxation of Mixed-integer Programs: Leveraging Logic Network Flow for Task and Motion Planning
This paper proposes an optimization-based task and motion planning framework, named "Logic Network Flow", that integrates temporal logic specifications into mixed-integer programs for efficient robot planning. Inspired b…
Motion PlanningA separation logic for sequences in pointer programs and its decidability
Separation logic and its variants can describe various properties on pointer programs. However, when it comes to properties on sequences, one may find it hard to formalize. To deal with properties on variable-length sequ…
Logical ReasoningBayesian Logic Programs
Bayesian networks provide an elegant formalism for representing and reasoning about uncertainty using probability theory. Theyare a probabilistic extension of propositional logic and, hence, inherit some of the limitatio…
Reasoning About the Transfer of Control
We present DCL-PC: a logic for reasoning about how the abilities of agents and coalitions of agents are altered by transferring control from one agent to another. The logical foundation of DCL-PC is CL-PC, a logic for re…
On the generalization of learned constraints for ASP solving in temporal domains
The representation of a dynamic problem in ASP usually boils down to using copies of variables and constraints, one for each time stamp, no matter whether it is directly encoded or via an action or temporal language. The…