Facts Do Not Cease to Exist Because They Are Ignored: Relativised Uniform Equivalence with Answer-Set Projection

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

This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.