A wide variety of nonmonotonic semantics can be expressed as approximators defined under AFT (Approximation Fixpoint Theory). Using traditional AFT theory, it is not possible to define approximators that rely on information computed in previous iterations of stable revision. However, this information is rich for semantics that incorporate classical negation into nonmonotonic reasoning. In this work, we introduce a methodology resembling AFT that can utilize priorly computed upper bounds to more precisely capture semantics. We demonstrate our framework's applicability to hybrid MKNF (minimal knowledge and negation as failure) knowledge bases by extending the state-of-the-art approximator.

We provide a comprehensive elaboration of the theoretical foundations of variable instantiation, or grounding, in Answer Set Programming (ASP). Building on the semantics of ASP's modeling language, we introduce a formal characterization of grounding algorithms in terms of (fixed point) operators. A major role is played by dedicated well-founded operators whose associated models provide semantic guidance for delineating the result of grounding along with on-the-fly simplifications. We address an expressive class of logic programs that incorporates recursive aggregates and thus amounts to the scope of existing ASP modeling languages. This is accompanied with a plain algorithmic framework detailing the grounding of recursive aggregates. The given algorithms correspond essentially to the ones used in the ASP grounder gringo.

In this paper, we explore the issue of inconsistency handling over prioritized knowledge bases (KBs), which consist of an ontology, a set of facts, and a priority relation between conflicting facts. In the database setting, a closely related scenario has been studied and led to the definition of three different notions of optimal repairs (global, Pareto, and completion) of a prioritized inconsistent database. After transferring the notions of globally-, Pareto- and completion-optimal repairs to our setting, we study the data complexity of the core reasoning tasks: query entailment under inconsistency-tolerant semantics based upon optimal repairs, existence of a unique optimal repair, and enumeration of all optimal repairs. Our results provide a nearly complete picture of the data complexity of these tasks for ontologies formulated in common DL-Lite dialects. The second contribution of our work is to clarify the relationship between optimal repairs and different notions of extensions for (set-based) argumentation frameworks. Among our results, we show that Pareto-optimal repairs correspond precisely to stable extensions (and often also to preferred extensions), and we propose a novel semantics for prioritized KBs which is inspired by grounded extensions and enjoys favourable computational properties. Our study also yields some results of independent interest concerning preference-based argumentation frameworks.

Abstract Dialectical Frameworks (ADFs) are argumentation frameworks where each node is associated with an acceptance condition. This allows us to model different types of dependencies as supports and attacks. Previous studies provided a translation from Normal Logic Programs (NLPs) to ADFs and proved the stable models semantics for a normal logic program has an equivalent semantics to that of the corresponding ADF. However, these studies failed in identifying a semantics for ADFs equivalent to a three-valued semantics (as partial stable models and well-founded models) for NLPs. In this work, we focus on a fragment of ADFs, called Attacking Dialectical Frameworks (ADF$^+$s), and provide a translation from NLPs to ADF$^+$s robust enough to guarantee the equivalence between partial stable models, well-founded models, regular models, stable models semantics for NLPs and respectively complete models, grounded models, preferred models, stable models for ADFs. In addition, we define a new semantics for ADF$^+$s, called L-stable, and show it is equivalent to the L-stable semantics for NLPs. This paper is under consideration for acceptance in TPLP.

Artificial Intelligence (AI) approaches to problem-solving and decision-making are becoming more and more complex, leading to a decrease in the understandability of solutions. The European Union's new General Data Protection Regulation tries to tackle this problem by stipulating a "right to explanation" for decisions made by AI systems. One of the AI paradigms that may be affected by this new regulation is Answer Set Programming (ASP). Thanks to the emergence of efficient solvers, ASP has recently been used for problem-solving in a variety of domains, including medicine, cryptography, and biology. To ensure the successful application of ASP as a problem-solving paradigm in the future, explanations of ASP solutions are crucial. In this survey, we give an overview of approaches that provide an answer to the question of why an answer set is a solution to a given problem, notably off-line justifications, causal graphs, argumentative explanations and why-not provenance, and highlight their similarities and differences. Moreover, we review methods explaining why a set of literals is not an answer set or why no solution exists at all.

A consequence of a logic program is a consistent set of literals that are satisfied by every answer set. The well-founded model is a consequence that can be used to simplify the logic program. In this paper, we extend the notion of well-founded models to consequences for simplifying disjunctive logic programs (DLPs) in a general manner. Specifically, we provide two main notions, strong reliable set and weak reliable set, and show that a DLP is strongly equivalent to the simplified program if and only if the consequence is a strong reliable set, and they have the same answer sets if and only if the consequence is a weak reliable set. Then we provide computational complexity on identifying both notions. In addition, we provide an algorithm to compute some strong reliable sets and show that the approach is an extension of the well-founded model in simplifying logic programs.

Declarative logic programs (LP) based on the well-founded semantics (WFS) are widely used for knowledge representation (KR).  Logical functions are desirable expressively in KR, but when present make LP inferencing become undecidable. In this paper, we present radial restraint : a novel approach to bounded rationality in LP. Radial restraint is parameterized by a norm that measures the syntactic complexity of a term, along with an abstraction function based on that norm.  When a term exceeds a bound for the norm, the term is assigned the WFS's third truth-value of undefined .  If the norm is finitary, radial restraint guarantees finiteness of models and decidability of inferencing, even when logical functions are present.  It further guarantees soundness, even when non-monotonicity is present.  We give a fixed-point semantics for radially restrained well-founded models which soundly approximate well-founded models.  We also show how to perform correct inferencing relative to such models, via SLG_ABS, an extension of tabled SLG resolution that uses norm-based abstraction functions.  Finally we discuss how SLG_ABS is implemented in the engine of XSB Prolog, and scales to knowledge bases with more than 10^8 rules and facts.

This paper considers the fragment ∃∀SO of second-order logic. Many interesting problems, such as conformant planning, can be naturally expressed as finite domain satisfiability problems of this logic. Such satisfiability problems are computationally hard (ΣP2) and many of these problems are often solved approximately. In this paper, we develop a general approximative method, i.e., a sound but incomplete method, for solving ∃∀SO satisfiability problems. We use a syntactic representation of a constraint propagation method for first-order logic to transform such an ∃∀SO satisfiability problem to an ∃SO(ID) satisfiability problem (second-order logic, extended with inductive definitions). The finite domain satisfiability problem for the latter language is in NP and can be handled by several existing solvers. Inductive definitions are a powerful knowledge representation tool, and this moti- vates us to also approximate ∃∀SO(ID) problems. In order to do this, we first show how to perform propagation on such inductive definitions. Next, we use this to approximate ∃∀SO(ID) satisfiability problems. All this provides a general theoretical framework for a number of approximative methods in the literature. Moreover, we also show how we can use this framework for solving practical useful problems, such as conformant planning, in an effective way.

Logic programs with abstract constraint atoms proposed by Marek and Truszczynski are very general logic programs.They are general enough to captureaggregate logic programs as well asrecently proposed description logic programs.In this paper, we propose a well-founded semantics for basic logic programs with arbitrary abstract constraint atoms, which are sets of rules whose heads have exactly one atom. Weshow that similar to the well-founded semanticsof normal logic programs, it has many desirable properties such as that it can becomputed in polynomial time, and is always correct with respect to theanswer set semantics. This paves the way for using our well-founded semanticsto simplify these logic programs. We also show how our semantics can be applied toaggregate logic programs and description logic programs, and compare itto the well-founded semantics already proposed for these logic programs.

The logic FO(ID) uses ideas from the field of logic programming to extend first order logic with non-monotone inductive definitions. Such logic formally extends logic programming, abductive logic programming and datalog, and thus formalizes the view on these formalisms as logics of (generalized) inductive definitions. The goal of this paper is to study a deductive inference method for PC(ID), which is the propositional fragment of FO(ID). We introduce a formal proof system based on the sequent calculus (Gentzen-style deductive system) for this logic. As PC(ID) is an integration of classical propositional logic and propositional inductive definitions, our sequent calculus proof system integrates inference rules for propositional calculus and definitions. We present the soundness and completeness of this proof system with respect to a slightly restricted fragment of PC(ID). We also provide some complexity results for PC(ID). By developing the proof system for PC(ID), it helps us to enhance the understanding of proof-theoretic foundations of FO(ID), and therefore to investigate useful proof systems for FO(ID).