Model-based recasting in answer-set programming

摘要

As is well known, answer-set programs do not satisfy the replacement property in general, i.e., programs P and Q that are equivalent may cease to be so when they are put in the context of some other program R, i.e., RUP and RUQ may have different (sets of) answer sets. Lifschitz, Pearce, and Valverde (2001) thus introduced strong equivalence for context-independent equivalence, and proved that such equivalence holds between given programs P and Q iff P and Q are equivalent theories in the monotonic logic of here-and-there. In this article, we consider a related question: given a program P, does there exist some program Q from a certain class C of programs such that P and Q are equivalent under a given notion of equivalence? Furthermore, if the answer to this question is positive, how can we recast P as an equivalent program from C (i.e., construct such a 0? In particular, we consider classes of programs that emerge by (dis)allowing disjunction and/or negation, and as equivalence notions we consider strong, uniform, and ordinary equivalence. Based on general model-theoretic properties and a novel form of canonical programs, we develop semantic characterisations for the existence of such a program Q, determine the computational complexity of checking existence, and provide (local) rewriting rules for recasting.