Igor Stéphan

Pedro Cabalar, Martín Diéguez, David Fernández-Duque et al.

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.

Martín Diéguez, Susana Hahn, Torsten Schaub et al.

Metric temporal equilibrium logic (\MEL) extends temporal equilibrium logic (\TEL) by incorporating quantitative timing constraints, enabling the specification and analysis of deadlines and durations. \MEL\ is particularly suited for domains where time-bound properties are crucial, such as embedded systems, cyber-physical systems, and real-time software. It facilitates the precise expression of timing behaviors, such as the requirement that an event must occur within 5 milliseconds of a trigger, which often elude traditional qualitative temporal logics. In this paper, we present a Tseitin-like translation that maps any metric temporal formula into a logic programming fragment restricted to past operators. This translation provides a formal bridge to leverage existing Answer Set Programming (ASP) solvers for reasoning about metric temporal constraints. By restricting the target fragment to past operators, we enable more effective evaluation and integration with current ASP-based toolchains for multi-shot solving.

Pedro Cabalar, Martín Diéguez, François Olivier et al.

Reasoning about dynamic systems with a fine-grained temporal and numeric resolution presents significant challenges for logic-based approaches like Answer Set Programming (ASP). To address this, we introduce and elaborate upon a novel temporal and constraint-based extension of the logic of Here-and-There and its nonmonotonic equilibrium extension, representing, to the best of our knowledge, the first approach to nonmonotonic temporal reasoning with constraints specifically tailored for ASP. This expressive system is achieved by a synergistic combination of two foundational ASP extensions: the linear-time logic of Here-and-There, providing robust nonmonotonic temporal reasoning capabilities, and the logic of Here-and-There with constraints, enabling the direct integration and manipulation of numeric constraints, among others. This work establishes the foundational logical framework for tackling complex dynamic systems with high resolution within the ASP paradigm.

Claire Lefèvre, Christopher Béatrix, Igor Stéphan et al.

The natural way to use Answer Set Programming (ASP) to represent knowledge in Artificial Intelligence or to solve a combinatorial problem is to elaborate a first order logic program with default negation. In a preliminary step this program with variables is translated in an equivalent propositional one by a first tool: the grounder. Then, the propositional program is given to a second tool: the solver. This last one computes (if they exist) one or many answer sets (stable models) of the program, each answer set encoding one solution of the initial problem. Until today, almost all ASP systems apply this two steps computation. In this article, the project ASPeRiX is presented as a first order forward chaining approach for Answer Set Computing. This project was amongst the first to introduce an approach of answer set computing that escapes the preliminary phase of rule instantiation by integrating it in the search process. The methodology applies a forward chaining of first order rules that are grounded on the fly by means of previously produced atoms. Theoretical foundations of the approach are presented, the main algorithms of the ASP solver ASPeRiX are detailed and some experiments and comparisons with existing systems are provided.