Applying Visible Strong Equivalence in Answer-Set Program Transformations

Abstract

Strong equivalence is one of the basic notions of equivalence that have been proposed for logic programs subject to the answer-set semantics. In this article, we propose a new generalization of strong equivalence (SE) that takes the visibility of atoms into account and we characterize it in terms of appropriately revised SE-models. Our design resembles (relativized) strong equivalence but is substantially different due to adopting a strict one-to-one correspondence of models from the notion of visible equivalence. We additionally tailor the characterization for more convenient use with positive programs and provide formal tools to exploit the tailored version also in the case of some programs that use negation. We illustrate the use of visible strong equivalence and the characterizations in showing the correctness of program transformations that make use of atom visibility. Moreover, we present a translation that enables us to automate the task of verifying visible strong equivalence for particular fragments of answer-set programs. We experimentally study the efficiency of verification when the goal is to check whether an extended rule is visibly strongly equivalent to its normalization, i.e., a subprogram expressing the original rule in terms of normal rules only. In the process, we verify the outputs of several real implementations of normalization schemes on a considerable number of input rules.