Uniform Equivalence for Equilibrium Logic and Logic Programs

For a given semantics, two logic programs Π₁ and Π₂ can be said to be equivalent if they have the same intended models and strongly equivalent if for any program X, Π₁ ∪ X and Π₂ ∪ X are equivalent. Eiter and Fink have recently studied and characterised under answer set semantics a further, related property of uniform equivalence, where the extension X is required to be a set of atoms. We extend their main results to propositional theories in equilibrium logic and describe a tableaux proof system for checking the property of uniform equivalence. We also show that no new forms of equivalence are obtained by varying the logical form of expressions in the extension X. Finally, some examples are studied including special cases of nested and generalized rules.