aalto1 untyped-item.component.html
Applying Visible Strong Equivalence in Answer-Set Program Transformations
Loading...
Access rights
openAccess
publishedVersion
URL
Journal Title
Journal ISSN
Volume Title
A1 Alkuperäisartikkeli tieteellisessä aikakauslehdessä
This publication is imported from Aalto University research portal.
View publication in the Research portal (opens in new window)
View/Open full text file from the Research portal (opens in new window)
View publication in the Research portal (opens in new window)
View/Open full text file from the Research portal (opens in new window)
Unless otherwise stated, all rights belong to the author. You may download, display and print this publication for Your own personal use. Commercial use is prohibited.
Date
Major/Subject
Mcode
Degree programme
Language
en
Pages
41
Series
ACM Transactions on Computational Logic, Volume 21, issue 4
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.
Description
Other note
Citation
Bomanson, J, Janhunen, T & Niemelä, I 2020, 'Applying Visible Strong Equivalence in Answer-Set Program Transformations', ACM Transactions on Computational Logic, vol. 21, no. 4, 33. https://doi.org/10.1145/3412854