Metric temporal equilibrium logic () extends temporal equilibrium logic () by incorporating quantitative timing constraints, enabling the specification and analysis of deadlines and durations. 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.

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.

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.

We shift the QCSP (Quantified Constraint Satisfaction Problems) framework to the QCHR (Quantified Constraint Handling Rules) framework by enabling dynamic binder and access to user-defined constraints. QCSP offers a natural framework to express PSPACE problems as finite two-players games. But to define a QCSP model, the binder must be formerly known and cannot be built dynamically even if the worst case won't occur. To overcome this issue, we define the new QCHR formalism that allows to build the binder dynamically during the solving. Our QCHR models exhibit state-of-the-art performances on static binder and outperforms previous QCSP approaches when the binder is dynamic.

We define a new formalism, called $\beth$ CHR, which generalises the CHR formalism by introducing some meta-constraints, called behaviors, allowing us to easily specify problems modelling an adversary. We define a new language with a syntax and a proof-theoretical semantics as an extension of the syntax and semantics of the CHR language.

Quantified Answer Set Programming (QASP) extends Answer Set Programming (ASP) by allowing quantification over propositional variables, similar to Quantified Boolean Formulas (QBF). In this paper, we interpret models of QASP formulas in terms of policies, which represent decision-making strategies that determine how existentially quantified variables should be assigned, given the conditions set by universally quantified variables. As a main contribution, we present an algorithm for policy extraction under QASP semantics, inspired by the Equilibrium Logic semantics for general ASP theories.

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.

Constraint Answer Set Programming (CASP) combines Answer Set Programming (ASP) and Constraint Programming (CP) to offer a powerful framework for solving complex problems. While there exists various ways to represent CASP problems, fusing both in a way that benefits both communities remains difficult to this day. To address this, we propose to extend the Well Founded Semantics (WFS) to propositional constraint logic programs. To this end, we present an iterative process involving elementary rewriting transformations to simplify the program iteratively. Our method aims to give a better description of the interactions between ASP and CP inside of a constraint logic program.

We present in this paper a way to use the paradigm of Answer Set Programming (ASP) into the Constraint Handling Rules (CHR) paradigm. We present a translation of the ASP language to the Constraint Handling Rules language. The committed-choice principle of the CHR paradigm leads to choose the rule-oriented approach of answer set computation. Since CHR is a first-order logic programming paradigm, the initial grounding phase of most of the ASP solvers is not required. Our implementation compiles an ASP program to a CHR(Prolog) program or to a CHR(C++) program. Preliminary experiments of the latter present some interesting results on ASP programs with some large sets of facts. Since Constraint Handling Rules is a paradigm developed for the implementation of user-defined constraints, we show how some extensions of ASP may be easily implemented in CHR: we show this by example for the choice rule.

This chapter presents the family of logic programming languages in which computation is viewed as deduction in a logical formalism. We first present the foundation of logic programming with Horn clauses illustrated by the Prolog language. From this first concept are born numerous extensions; here we describe two of them in details: constraint logic programming which allows a more elegant treatment of domains other than finite terms and Answer Set Programming which gives a better treatment of negation and appears to be an effective implementation of non-monotonic reasoning.

This paper deals with querying ontology-based knowledge bases equipped with non-monotonic rules through a case study within the framework of Cultural Heritage. It focuses on 3D underwater surveys on the Xlendi wreck which is represented by an OWL2 knowledge base with a large dataset. The paper aims at improving the interactions between the archaeologists and the knowledge base providing new queries that involve non-monotonic rules in order to perform qualitative spatial reasoning. To this end, the knowledge base initially represented in OWL2-QL is translated into an equivalent Answer Set Programming (ASP) program and is enriched with a set of non-monotonic ASP rules suitable to express default and exceptions. An ASP query answering approach is proposed and implemented. Furthermore due to the increased expressiveness of non-monotonic rules it provides spatial reasoning and spatial relations between artifacts query answering which is not possible with query answering languages such as SPARQL and SQWRL.

Constraint handling rules are a committed-choice language consisting of multiple-heads guarded rules that rewrite constraints into simpler ones until they are solved. We propose a new prooftheoretical declarative linear semantics for Constraint Handling Rules. We demonstrate completeness and soundness of our semantics w.r.t. operational ωt semantics. We propose also a translation from this semantics to linear logic. 2012 ACM Subject Classification Theory of computation→ Constraint and logic programming

Ontologies are used to describe information about concepts and links between them. Several efficient reasoners are available for query answering with ontologies. When information to be processed is imperfect or is subject to exception, common formalisms are not suitable anymore, that is why we propose the use of Answer Set Programming (ASP) that offers a better expressivity for ontologies. We take interest in the formal definition of query answering in ASP and we show that related implementations give interesting results both on traditional ontologies and with those containing exceptions. MOTS-CLÉS : Answer Set Programming, interrogation, ontologie.

Belief base revision has been studied within the answer set programming framework. We go a step further by introducing uncertainty and studying belief base revision when beliefs are represented by possibilistic logic programs under possibilistic answer set semantics and revised by certain input. The paper proposes two approaches of rule-based revision operators and presents their semantic characterization in terms of possibilistic distribution. This semantic characterization allows for equivalently considering the evolution of syntactic logic programs and the evolution of their semantic content. It then studies the logical properties of the proposed operators and gives complexity results.

This article deals with the combination of ontologies and rules by means of existential rules and answer set programming. Existential rules have been proposed for representing ontological knowledge, specifically in the context of Ontology- Based Data Access. Furthermore Answer Set Programming (ASP) is an appropriate formalism to represent various problems issued from Artificial Intelligence and arising when available information is incomplete. The combination of the two formalisms requires to extend existential rules with nonmonotonic negation and to extend ASP with existential variables. In this article, we present the syntax and semantics of Existential Non Monotonic Rules (ENM-rules) using skolemization which join together the two frameworks. We formalize its links with standard ASP. Moreover, since entailment with existential rules is undecidable, we present conditions that ensure the termination of a breadth-first forward chaining algorithm known as the chase and we discuss extension of these results in the nonmonotonic case.

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.