Semi-equilibrium models for paracoherent answer set programs

摘要

The answer set semantics may assign a logic program to model, due to logical contradiction or unstable negation, which is caused by cyclic dependency of an atom on 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. In this paper, we give a model-theoretic characterization of semi-stable models, which makes the semantics more accessible. Motivated by some anomalies of semi-stable model semantics with respect to basic epistemic properties, we propose an amendment that satisfies these properties. 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. We consider refinements of this semantics to respect modularity in the rules, based on splitting sets, the major tool for modularity in modeling 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. 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.