Johannes Oetsch, Hans Tompits, Stefan Woltran
Recent research in answer-set programming (ASP) focuses on different notions of equivalence between programs which are relevant for program optimisation and modular programming. Prominent among these notions is uniform equivalence, which checks whether two programs have the same semantics when joined with an arbitrary set of facts. In this paper, we study a family of more fine-grained versions of uniform equivalence, where the alphabet of the added facts as well as the projection of answer sets is taken into account. The latter feature, in particular, allows the removal of auxiliary atoms in computation, which is important for practical programming aspects. We introduce novel semantic characterisations for the equivalence problems under consideration and analyse the computational complexity for checking these problems. We furthermore provide efficient reductions to quantified propositional logic, yielding a rapid-prototyping system for equivalence checking.
Subjects: 3.3 Nonmonotonic Reasoning; 9.2 Computational Complexity
Submitted: Apr 24, 2007