A Fixpoint Characterisation of Temporal Equilibrium Logic

Abstract

[Abstract]: Connections of intuitionistic and intermediate logics with logic programming have been extensively studied in the literature. Among the different results in the literature we find equilibrium logic (Pearce, 1996) and Safe beliefs (Osorio et al., 2005). Pearce’s approach admits a characterisation in terms of a fixpoint (consequence) operator on the here-and-there intermediate logic (Heyting, 1930), which is similar to the notion of theory completion in default and autoepistemic logics. Osorio’s safe beliefs are also given in terms of a fixpoint operator under intuitionistic logic semantics. In this latter case, intuitionistic logic can be replaced by any intermediate logic without altering the result.

In this paper we consider temporal equilibrium logic, an combination of equilibrium logic and linear-time temporal logic. In this context we extend Pearce’s and Osorio’s approach to temporal case and we discuss the relation of intuitionistic temporal logic and temporal logic programming.