As is well known, answer-set programs do not satisfy the replacement property in general, i.e., programs and that are equivalent may cease to be so when they are put in the context of some other program, i.e., and may have different answer sets. Lifschitz, Pearce, and Valverde thus introduced strong equivalence for context-independent equivalence, and proved that such equivalence holds between given programs and iff and are equivalent theories in the monotonic logic of here-and-there. In this article, we consider a (...) related question: given a program, does there exist some program from a certain class of programs such that and are equivalent under a given notion of equivalence? Furthermore, if the answer to this question is positive, how can we recast as an equivalent program from? In particular, we consider classes of programs that emerge by 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, determine the computational complexity of checking existence, and provide rewriting rules for recasting. (shrink)

Some investigations into the algebraic constructive aspects of a decision procedure for various fragments of Relevant Logics are presented. Decidability of these fragments relies on S. Kripke's gentzenizations and on his combinatorial lemma known as Kripke's lemma that B. Meyer has shown equivalent to Dickson's lemma in number theory and to his own infinite divisor lemma, henceforth, Meyer's lemma or IDP. These investigations of the constructive aspects of the Kripke's-Meyer's decision procedure originate in the development of Paul Thistlewaite's “Kripke” theorem (...) prover that had been devised to tackle the decision problem of the Relevant Logic R. A. Urquhart's pen and paper solution that relies on a sophisticated algebraic and geometric treatment of the problem shows the usefulness of an algebraic approach in Logic. Here, the study of the constructive aspects of the Kripke-Meyer decision procedure relies on various algebraic constructive results in the theory of polynomials rings. (shrink)