Applications of Intuitionistic Temporal Logic to Temporal Answer Set Programming
Authors: Pedro Cabalar, Martín Diéguez, David Fernández-Duque, François Laferrière, Torsten Schaub, Igor Stéphan
Organizations: University of Corunna, Spain · University of Angers, France · University of Barcelona, Spain · Potassco Solutions, Germany · University of Potsdam, Germany
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.
Figures & tables
Figure 1: A bisimulation relation, represented in red dashed lines, among two intuitionistic models M (on the left) and M′ (with a unique maximal world, on the right). We assume that, M,w⊨{¬p∨¬¬p∣p∈P} and we define V′ as V′(w):=V(w) , V′(vi):=V(vi) for all i∈{1,2,3} and V′(u) can be set (for instance) to V(u1) . Reflexivity and transitivity of ≼ and ≼′ is not represented for the sake of readability.
Figure 2: An intuitionistic model M , a HT model M′ and a bisimulations Z (in red dashed lines) among them. As preconditions, V(v)=T for all v∈W with v=w , V′(0)=V(w) and V′(1)=V(u) . Reflexivity and transitivity of ≼ and ≼′ are not represented for the sake of readability.
Figure 3: Diagrams associated to forward and backward confluence. The above diagrams can always be completed if S is forward or backward confluent (represented by means of dashed arrows).
Figure 4: Example of an ITLe model M=((W,≼,S),V) , where reflexivity and transitivity for ≼ are not represented.
Figure 5: Example of an ITLe model satisfying Γ:={¬\textopenbulletp,¬\textopenbullet¬p} . Reflexivity and transitivity of ≼ are omitted for the sake of clarity.
Figure 6: A ITLp model M satisfying Γ:={{□¬¬p,¬□p}} at (0,0) . The proposition p is true in the worlds displayed boldface while false in those that are not. Reflexivity and transitivity of ≼ are not represented for the sake of readability.
Figure 7: Two ITLBDn models M=⟨(W,≼,S),V⟩ and M′=⟨(W′,≼′,S′),V′⟩ . Under the assumption that M,w⊨{□(¬p∨¬¬p)∣p∈P} , for all i≥0 , all maximal worlds in ≼(Si(w)) satisfy the same atoms. By setting V′(v):=V(v) for every world v∈W∩W′ and, for all i≥0 , V′(ui):=V(x) , with x a maximal world in ≼(Si(w)) , it can be verified that the relation Z displayed in terms of red dashed lines is a bisimulation between M and M′ . The reflexivity and transitivity of ≼ and ≼′ is not represented for the sake of readability.
Figure 8: Example of model contraction. M=⟨(W,≼,S),V⟩ is an ITLBDn model and M′=⟨(N×{0,1},≼′,S′),V′⟩ is a THT model. Under the assumption that every world v∈≺(Si(w)) satisfies exactly the same set of propositional variables, we can set V′((i,0)):=V(wi) and V′((i,1)):=V(ui) , for all i≥0 . The relation Z , displayed in red dashed lines, is a bisimulation between M and M′ . The reflexivity and transitivity of ≼′ and ≼ is not represented for the sake of readability.
Answer Set Programming (ASP) is a declarative logic paradigm for representing nonmonotonic rules, constraints, and search problems through stable models.