To solve a problem in answer set programming (ASP), one constructs a logic program so that its answer sets correspond to the solutions of the problem and computes the answer sets of the program using a special purpose search engine. The encodings are not unique, i.e. several versions of a program can be used e.g. in optimizing the execution time or space. Since the solutions to the problem correspond to answer sets of the program, it is necessary to ensure that the different encodings yield the same output. In ASP this means that one has to check whether given two logic programs have the same answer sets, i.e., whether they are semantically equivalent. We consider in this work the class of disjunctive logic programs, that form a proper generalization of normal logic programs. \par The equivalence of logic programs $P$ and $Q$ can naturally be verified using an explicit cross-check of all the answer sets of both programs. Our aim is, however, to develop a systematic method for testing the equivalence so that a naive cross-check of answer sets is not needed. \par The idea is to translate logic programs $P$ and $Q$ into a single logic program that has an answer set if and only if $P$ has an answer set that is not an answer set of $Q$. Thus answer sets of the translation (if found), act as a counter-examples for the equivalence of $P$ and $Q$. The counter-examples for equivalence divide naturally in two types. Thus the search for counter-examples can be performed separately for both types using a two-phased translation. \par We have implemented the translation functions. Experiments with the implementation show that in several cases the translation-based approach is superior to the naive cross-checking approach, especially, if the programs to be tested have several answer sets and are likely to be nonequivalent. If the number of answer sets is low, then the naive cross-checking approach is likely to be faster. Furthermore, in general it is faster to use the two-phased translation.

@techreport{
    HUT-TCS-A85_eoikarin,
    author = "Oikarinen, Emilia",
    title = "Testing the Equivalence of Disjunctive Logic Programs",
    url = "http://www.tcs.hut.fi/Publications/info/bibdb.HUT-TCS-A85.shtml",
    abstract = "To solve a problem in answer set programming (ASP), one constructs a logic program so that its answer sets correspond to the solutions of the problem and computes the answer sets of the program using a special purpose search engine. The encodings are not unique, i.e. several versions of a program can be used e.g. in optimizing the execution time or space. Since the solutions to the problem correspond to answer sets of the program, it is necessary to ensure that the different encodings yield the same output. In ASP this means that one has to check whether given two logic programs have the same answer sets, i.e., whether they are semantically equivalent. We consider in this work the class of disjunctive logic programs, that form a proper generalization of normal logic programs. \par The equivalence of logic programs $P$ and $Q$ can naturally be verified using an explicit cross-check of all the answer sets of both programs. Our aim is, however, to develop a systematic method for testing the equivalence so that a naive cross-check of answer sets is not needed. \par The idea is to translate logic programs $P$ and $Q$ into a single logic program that has an answer set if and only if $P$ has an answer set that is not an answer set of $Q$. Thus answer sets of the translation (if found), act as a counter-examples for the equivalence of $P$ and $Q$. The counter-examples for equivalence divide naturally in two types. Thus the search for counter-examples can be performed separately for both types using a two-phased translation. \par We have implemented the translation functions. Experiments with the implementation show that in several cases the translation-based approach is superior to the naive cross-checking approach, especially, if the programs to be tested have several answer sets and are likely to be nonequivalent. If the number of answer sets is low, then the naive cross-checking approach is likely to be faster. Furthermore, in general it is faster to use the two-phased translation.",
    address = "Espoo, Finland",
    number = "A85",
    month = "December",
    flags = "SERIES-A public SA-53695 copy",
    pages = "61",
    year = "2003",
    keywords = "disjunctive logic programs, equivalence testing, stable model semantics, answer set programming, non-monotonic reasoning, computational complexity",
    type = "Research Report",
    institution = "Helsinki University of Technology, Laboratory for Theoretical Computer Science"
}

AUTHORS:

ABSTRACT:

URL:
http://www.tcs.hut.fi/Publications/info/bibdb.HUT-TCS-A85.shtml

AUTHORS:

ABSTRACT:

URL: http://www.tcs.hut.fi/Publications/info/bibdb.HUT-TCS-A85.shtml

URL:
http://www.tcs.hut.fi/Publications/info/bibdb.HUT-TCS-A85.shtml