A Generalized Gelfond-Lifschitz Transformation for Logic Programs with Abstract Constraints

Abstract

We present a generalized Gelfond-Lifschitz transformation in order to define stable models for a logic program with arbitrary abstract constraints on sets (c-atoms). The generalization is based on a formal semantics and a novel abstract representation of c-atoms, as opposed to the commonly used power set form representation. In many cases, the abstract representation of a c-atom results in a substantial reduction of size from its power set form representation. We show that any c-atom A =(Ad,Ac) in the body of a clause can be characterized using its satisfiable sets, so that given an interpretation I the c-atom can be handled simply by introducing a special atom θA together with a new clause θA ← A1,..., An for each satisfiable set A1,..., An of A. We also prove that the latest fixpoint approach presented by Son et al. and our approach using the generalized Gelfond-Lifschitz transformation are semantically equivalent in the sense that they define the same set of stable models.