Casting away disjunction and negation under a generalisation of strong equivalence with projection

Abstract

In answer-set programming (ASP), many notions of program equivalence have been introduced and formally analysed. A particular line of research in this direction aims at studying conditions under which certain syntactic constructs can be eliminated from programs preserving some given equivalence relation. In this paper, we continue this endeavour introducing novel conditions under which disjunction and negation can be eliminated from answer-set programs under relativised strong equivalence with projection. This notion is a generalisation of the usual strong-equivalence relation, as introduced by Lifschitz, Pearce, and Valverde, by allowing parametrisable context and output alphabets, which is an important feature in view of practical programming techniques like the use of local variables and modules. We provide model-theoretic conditions that hold for a disjunctive logic program P precisely when there is a program Q, equivalent to P under our considered notion, such that Q is either positive, normal, or Horn, respectively. Moreover, we outline how such a Q, called a casting of P, can be obtained, and consider complexity issues. © 2009 Springer Berlin Heidelberg.