Applying Visible Strong Equivalence in Answer-Set Program Transformations

Research output: Contribution to journalArticleScientificpeer-review

126 Downloads (Pure)

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.
Original languageEnglish
Article number33
Number of pages41
JournalACM TRANSACTIONS ON COMPUTATIONAL LOGIC
Volume21
Issue number4
DOIs
Publication statusPublished - Oct 2020
MoE publication typeA1 Journal article-refereed

Keywords

  • stable models
  • strong equivalence
  • hidden atoms
  • auxiliary atoms
  • program transformations
  • normalizations

Fingerprint Dive into the research topics of 'Applying Visible Strong Equivalence in Answer-Set Program Transformations'. Together they form a unique fingerprint.

Cite this