Reference:
Emilia Oikarinen. Testing the equivalence of disjunctive logic programs. Research Report A85, Helsinki University of Technology, Laboratory for Theoretical Computer Science, Espoo, Finland, December 2003.
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.
The equivalence of logic programs and can naturally be verified using an explicit crosscheck 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 crosscheck of answer sets is not needed.
The idea is to translate logic programs and into a single logic program that has an answer set if and only if has an answer set that is not an answer set of . Thus answer sets of the translation (if found), act as a counterexamples for the equivalence of and . The counterexamples for equivalence divide naturally in two types. Thus the search for counterexamples can be performed separately for both types using a twophased translation.
We have implemented the translation functions. Experiments with the implementation show that in several cases the translationbased approach is superior to the naive crosschecking 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 crosschecking approach is likely to be faster. Furthermore, in general it is faster to use the twophased translation.
Keywords:
disjunctive logic programs, equivalence testing, stable model semantics, answer set programming, nonmonotonic reasoning, computational complexity
Suggested BibTeX entry:
@techreport{HUTTCSA85,
address = {Espoo, Finland},
author = {Emilia Oikarinen},
institution = {Helsinki University of Technology, Laboratory for Theoretical Computer Science},
month = {December},
number = {A85},
pages = {61},
title = {Testing the Equivalence of Disjunctive Logic Programs},
type = {Research Report},
year = {2003},
}
