By Giovanni Amendola,
Università della Calabria
December 2016
Abstract
Answer Set Programming (ASP) is a declarative programming paradigm based on the stable model semantics. The idea of ASP is to encode a computational problem into a logic problem, whose stable models, called also answer sets, correspond to the solution of the original problem.
The answer set semantics may assign a logic program no model, due to logical contradiction or unstable negation, which is caused by cyclic dependency of an atom from its negation. While logical contradictions can be handled with traditional techniques from paraconsistent reasoning, instability requires other methods. We consider resorting to a paracoherent semantics, in which 3-valued interpretations are used where a third truth value besides true and false expresses that an atom is believed true. This is at the basis of the semi-stable model semantics, which was defined using a program transformation.
This thesis has, as starting point, a paper presented in 2010 at the 12th “International Conference on Principles of Knowledge Representation and Reasoning”, where a model-theoretic characterization of semi-stable models, which makes the semantics more accessible is given. Motivated by some anomalies of semi-stable model semantics with respect to basic epistemic properties, an amendment that satisfies these properties is proposed. The latter has both a transformational and a model-theoretic characterization that reveals it as a relaxation of equilibrium logic, the logical reconstruction of answer set semantics, and is thus called the semi-equilibrium model semantics.
In this thesis, we consider refinements of this semantics to respect modularity in the rules, based on splitting sets, the major tool for modularity in modelling and evaluating answer set programs. In that, we single out classes of canonical models that are amenable for customary bottom-up evaluation of answer set programs, with an option to switch to a paracoherent mode when lack of an answer set is detected.
A complexity analysis of major reasoning tasks shows that semi-equilibrium models are harder than answer sets (i.e., equilibrium models), due to a global minimization step for keeping the gap between true and believed true atoms as small as possible. Then, we consider different algorithms to compute semi-stable and semi-equilibrium models, implementing and integrating them into an answer set building framework. Moreover, we report results of experimental activity conducted on benchmarks from ASP competitions, identifying the more efficient algorithm.
Our results contribute to the logical foundations of paracoherent answer set programming, which gains increasing importance in inconsistency management, and at the same time provide a basis for algorithm development and integration into answer set solvers.