Solving a problem in the answer set programming approach means constructing a logic program so that the answer sets of the program correspond to the solutions to the problem. Typically, a programmer develops a series of improved formulations for a particular problem. Consequently, the programmer is confronted by another problem, namely ensuring that subsequent formulations are equivalent, i.e., give rise to the same answer sets. To ease answer set programming, we propose a methodology for testing the equivalence of logic programs. The basic idea is to translate the logic programs $P$ and $Q$ under consideration into a single logic program $R$ whose answer sets (if such exist) yield counter-examples to the equivalence of $P$ and $Q$. The translation function presented in the paper has been implemented as a translator program LPEQ that enables the equivalence testing of logic programs using the SMODELS system. Experiments performed with LPEQ and SMODELS suggest that establishing the equivalence of logic programs in this way is in certain cases much faster than explicit cross-checking of answer sets.

@inproceedings{
    JO02:jelia_eoikarin,
    editor = "Flesca, Sergio and Greco, Sergio and Leone, Nicola and Ianni, Giovambattista",
    author = "Janhunen, Tomi and Oikarinen, Emilia",
    publisher = "Springer-Verlag",
    title = "Testing the Equivalence of Logic Programs under Stable Model Semantics",
    url = "http://www.springerlink.com/content/8p61lh1x02q2jan6",
    series = "Lecture Notes in Artificial Intelligence",
    booktitle = "Logics in Artificial Intelligence, Proceedings of the 8th European Conference",
    year = "2002",
    month = "September",
    volume = "2424",
    flags = "copy SA-53695",
    pages = "493--504",
    address = "Cosenza, Italy",
    abstract = "Solving a problem in the answer set programming approach means constructing a logic program so that the answer sets of the program correspond to the solutions to the problem. Typically, a programmer develops a series of improved formulations for a particular problem. Consequently, the programmer is confronted by another problem, namely ensuring that subsequent formulations are equivalent, i.e., give rise to the same answer sets. To ease answer set programming, we propose a methodology for testing the equivalence of logic programs. The basic idea is to translate the logic programs $P$ and $Q$ under consideration into a single logic program $R$ whose answer sets (if such exist) yield counter-examples to the equivalence of $P$ and $Q$. The translation function presented in the paper has been implemented as a translator program LPEQ that enables the equivalence testing of logic programs using the SMODELS system. Experiments performed with LPEQ and SMODELS suggest that establishing the equivalence of logic programs in this way is in certain cases much faster than explicit cross-checking of answer sets."
}

AUTHORS:

ABSTRACT:

URL:
http://www.springerlink.com/content/8p61lh1x02q2jan6

AUTHORS:

ABSTRACT:

URL: http://www.springerlink.com/content/8p61lh1x02q2jan6

URL:
http://www.springerlink.com/content/8p61lh1x02q2jan6