Applications of Intuitionistic Temporal Logic to Temporal Answer Set Programming
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.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Intuitionistic Linear Temporal Logics
We consider intuitionistic variants of linear temporal logic with `next', `until' and `release' based on expanding posets: partial orders equipped with an order-preserving transition function. This class of structures gi…
Gödel-Dummett linear temporal logic
We investigate a version of linear temporal logic whose propositional fragment is G\"odel-Dummett logic (which is well known both as a superintuitionistic logic and a t-norm fuzzy logic). We define the logic using two na…
validTopological and Algebraic Structures of Atanassov's Intuitionistic Fuzzy-Values Space
We prove that the space of intuitionistic fuzzy values (IFVs) with a linear order based on a score function and an accuracy function has the same algebraic structure as the one induced by a linear order based on a simila…
NegationReasoning about Intuitionistic Computation Tree Logic
In this paper, we define an intuitionistic version of Computation Tree Logic. After explaining the semantic features of intuitionistic logic, we examine how these characteristics can be interesting for formal verificatio…
validDeriving Theorems in Implicational Linear Logic, Declaratively
The problem we want to solve is how to generate all theorems of a given size in the implicational fragment of propositional intuitionistic linear logic. We start by filtering for linearity the proof terms associated by o…
Automated Theorem Proving