Testing the Equivalence of Logic Programs under Stable Model Semantics

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.

The research reported in this paper is affiliated with the project “Applications of Rule-Based Constraint Programming” (#53695) funded by the Academy of Finland.