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.
The development of temporal extensions of Answer Set Programming (ASP) has led to the emergence of non-monotonic linear-time (TEL), dynamic (DEL), and metric (MEL) temporal equilibrium logics. However, the inherent rigidity of highly optimized ASP systems often hinders the rapid exploration and implementation of alternative logical designs. In this work, we propose a flexible meta-programming framework that operationalizes the semantics of varied temporal logics through a unified, declarative framework. Our approach extends standard ASP meta-programming by augmenting clingo's theory grammar with formal type specifications and nesting capabilities. To ensure semantic correctness, we introduce a transformation pipeline that protects nested modalities from stable-model-based simplifications during grounding. We demonstrate the extensibility of our framework by implementing meta-encodings for TEL, MEL, and DEL. We provide a comprehensive account of TEL and highlight the key features for managing the interval constraints of MEL and the Fischer-Ladner closure in DEL. Finally, we introduce the metasp system, a versatile tool that encapsulates this workflow.
Susana Hahn, Amadé Nemes, Javier Romero +1
University of Potsdam, Germany · Potassco Solutions, Germany
By leveraging large-scale pretraining, LLMs can interpret diverse temporal expressions and question formulations without task-specific training. However, existing prompt-based neuro-symbolic systems continue to rely on LLMs for both semantic interpretation and exact temporal inference. Consequently, discrete decisions regarding intervals, time anchors, and ordered states remain vulnerable to probabilistic errors and difficult to verify. We present STAIR, a Semantic-Temporal Automaton for Interpretable Reasoning. STAIR separates semantic interpretation from precise temporal inference: an answer-free LLM adapter maps complex question formulations to normalized temporal intents, while a deterministic temporal automaton with finite control and guarded transitions executes the corresponding policies over canonicalized evidence. Following a rule-first design, STAIR resolves standard questions without invoking an LLM and applies semantic adaptation only when the rule path fails to produce an executable intent. This approach reduces free-form reasoning, making temporal decisions verifiable and interpretable. Specifically, guarded execution supports precise point-time containment and before/after selection, while semantic adaptation handles non-exact intervals and time-anchored queries. Across the TimeQA-Easy, TimeQA-Hard, TempReason-L2, and TempReason-L3 datasets, STAIR consistently outperforms strong baselines in the TQA task using matched model settings, achieving average F1 improvements of 16.57% and 3.10% when utilizing the Qwen2.5-7B and GPT-4o-mini models, respectively. Furthermore, ablations and diagnostic analyses demonstrate that STAIR excels at handling both boundary-sensitive and order-sensitive queries, while its guarded execution and semantic adaptation ensure precise point-time reasoning and inexact intervals, respectively.
Xinlong Dai, Jinchuan Zhang, Lei Gao +3
University of Electronic Science and Technology of China (UESTC)
We introduce Qiana, a logic framework for reasoning on formulas that are true only in specific contexts. In Qiana, it is possible to quantify over both formulas and contexts to express, e.g., that ``everyone knows everything Alice says''. Qiana also permits paraconsistent logics within contexts, so that contexts can contain contradictions. Furthermore, Qiana is based on first-order logic, and is finitely axiomatizable, so that Qiana theories are compatible with pre-existing first-order logic theorem provers. We show how Qiana can be used to represent temporality, event calculus, and modal logic. We also discuss different design alternatives of Qiana.
Simon Coumes, Pierre-Henri Paris, François Schwarzentruber +1
LTCI, LaHDAK · Telecom Paris, Institut Polytechnique de Paris, France · Université Paris-Saclay, France +3