Applications of Intuitionistic Temporal Logic to Temporal Answer Set Programming

TL;DR

This paper explores the theoretical foundations of Temporal Answer Set Programming by extending intuitionistic and intermediate logics with temporal operators, establishing a formal link between temporal logic and logic programming.

Contribution

It introduces Temporal Equilibrium Logic, combining equilibrium logic with linear-time temporal operators, and generalizes prior static approaches to the temporal setting.

Findings

Established a formal correspondence between temporal intuitionistic logic and temporal logic programming.

Deepened the theoretical understanding of Temporal Answer Set Programming.

Provided new frameworks for reasoning about temporal information in logic programming.

Abstract

The relationship between intuitionistic or intermediate logics and logic programming has been extensively studied, prominently featuring Pearce's equilibrium logic and Osorio's safe beliefs. Equilibrium logic admits a fixpoint characterization based on the logic of here-and-there, akin to theory completion in default and autoepistemic logics. Safe beliefs are similarly defined via a fixpoint operator, albeit under the semantics of intuitionistic or other intermediate logics. In this paper, we investigate the logical foundations of Temporal Answer Set Programming through the lens of Temporal Equilibrium Logic, a formalism combining equilibrium logic with linear-time temporal operators. We lift the seminal approaches of Pearce and Osorio to the temporal setting, establishing a formal correspondence between temporal intuitionistic logic and temporal logic programming. Our results deepen the theoretical underpinnings of Temporal Answer Set Programming and provide new avenues for research in temporal reasoning.