Over the last couple of decades, there has been a considerable effort devoted to the problem of updating logic programs under the stable model semantics (a.k.a. answer-set programs) or, in other words, the problem of characterising the result of bringing up-to-date a logic program when the world it describes changes. Whereas the state-of-the-art approaches are guided by the same basic intuitions and aspirations as belief updates in the context of classical logic, they build upon fundamentally different principles and methods, which have prevented a unifying framework that could embrace both belief and rule updates. In this paper, we will overview some of the main approaches and results related to answer-set programming updates, while pointing out some of the main challenges that research in this topic has faced.

Answer set programming (ASP) is an efficient problem-solving approach, which has been strongly supported both scientifically and technologically by several solvers, ongoing active research, and implementations in many different fields. However, although researchers acknowledged long ago the necessity of epistemic operators in the language of ASP for better introspective reasoning, this research venue did not attract much attention until recently. Moreover, the existing epistemic extensions of ASP in the literature are not widely approved either, due to the fact that some propose unintended results even for some simple acyclic epistemic programs, new unexpected results may possibly be found, and more importantly, researchers have different reasonings for some critical programs. To that end, Cabalar et al. have recently identified some structural properties of epistemic programs to formally support a possible semantics proposal of such programs and standardise their results. Nonetheless, the soundness of these properties is still under debate, and they are not widely accepted either by the ASP community. Thus, it seems that there is still time to really understand the paradigm, have a mature formalism, and determine the principles providing formal justification of their understandable models. In this paper, we mainly focus on the existing semantics approaches, the criteria that a satisfactory semantics is supposed to satisfy, and the ways to improve them. We also extend some well-known propositions of here-and-there logic (HT) into epistemic HT so as to reveal the real behaviour of programs. Finally, we propose a slightly novel semantics for epistemic ASP, which can be considered as a reflexive extension of Cabalar et al.'s recent formalism called autoepistemic ASP.

Forgetting - or variable elimination - is an operation that allows the removal, from a knowledge base, of middle variables no longer deemed relevant. In recent years, many different approaches for forgetting in Answer Set Programming have been proposed, in the form of specific operators, or classes of such operators, commonly following different principles and obeying different properties. Each such approach was developed to somehow address some particular view on forgetting, aimed at obeying a specific set of properties deemed desirable in such view, but a comprehensive and uniform overview of all the existing operators and properties is missing. In this paper, we thoroughly examine existing properties and (classes of) operators for forgetting in Answer Set Programming, drawing a complete picture of the landscape of these classes of forgetting operators, which includes many novel results on relations between properties and operators, including considerations on concrete operators to compute results of forgetting and computational complexity. Our goal is to provide guidance to help users in choosing the operator most adequate for their application requirements.

Weighted Logic is a powerful tool for the specification of calculations over semirings that depend on qualitative information. Using a novel combination of Weighted Logic and Here-and-There (HT) Logic, in which this dependence is based on intuitionistic grounds, we introduce Answer Set Programming with Algebraic Constraints (ASP(A C)), where rules may contain constraints that compare semiring values to weighted formula evaluations. Such constraints provide streamlined access to a manifold of constructs available in ASP, like aggregates, choice constraints, and arithmetic operators. They extend some of them and provide a generic framework for defining programs with algebraic computation, which can be fruitfully used e.g. for provenance semantics of datalog programs. While undecidable in general, expressive fragments of ASP(A C) can be exploited for effective problem solving in a rich framework. This work is under consideration for acceptance in Theory and Practice of Logic Programming.

Different notions of equivalence, such as the prominent notions of strong and uniform equivalence, have been studied in Answer-Set Programming, mainly for the purpose of identifying programs that can serve as substitutes without altering the semantics, for instance in program optimization. Such semantic comparisons are usually characterized by various selections of models in the logic of Here-and-There (HT). For uniform equivalence however, correct characterizations in terms of HT-models can only be obtained for finite theories, respectively programs. In this article, we show that a selection of countermodels in HT captures uniform equivalence also for infinite theories. This result is turned into coherent characterizations of the different notions of equivalence by countermodels, as well as by a mixture of HT-models and countermodels (so-called equivalence interpretations). Moreover, we generalize the so-called notion of relativized hyperequivalence for programs to propositional theories, and apply the same methodology in order to obtain a semantic characterization which is amenable to infinite settings. This allows for a lifting of the results to first-order theories under a very general semantics given in terms of a quantified version of HT. We thus obtain a general framework for the study of various notions of equivalence for theories under answer-set semantics. Moreover, we prove an expedient property that allows for a simplified treatment of extended signatures, and provide further results for non-ground logic programs. In particular, uniform equivalence coincides under open and ordinary answer-set semantics, and for finite non-ground programs under these semantics, also the usual characterization of uniform equivalence in terms of maximal and total HT-models of the grounding is correct, even for infinite domains, when corresponding ground programs are infinite.

We study the problem of reasoning from incoherent answer set programs, i.e., from logic programs that do not have an answer set due to cyclic dependencies of an atom from its default negation. As a starting point we consider so-called semi-stable models which have been developed for this purpose building on a program transformation, called epistemic transformation. We give a model-theoretic characterization of this semantics, considering pairs of two-valued interpretations of the original program, rather than resorting to its epistemic transformation. Moreover, we show some anomalies of semi-stable semantics with respect to basic epistemic properties and propose an alternative semantics satisfying these properties. In addition to a model-theoretic and a transformational characterization of the alternative semantics, we prove precise complexity results for main reasoning tasks under both semantics.