Semantical Characterizations and Complexity of Equivalences in Answer Set Programming

TL;DR

This paper explores various notions of program equivalence in answer set programming, providing semantic characterizations and complexity analyses to enhance optimization and modularity in logic programming.

Contribution

It introduces and analyzes uniform and relativized equivalences for disjunctive logic programs, extending existing concepts and offering new complexity results.

Findings

Semantic characterizations of different equivalence notions

Complexity classifications for equivalence checking

Extensions to answer set semantics with strong negation

Abstract

In recent research on non-monotonic logic programming, repeatedly strong equivalence of logic programs P and Q has been considered, which holds if the programs P union R and Q union R have the same answer sets for any other program R. This property strengthens equivalence of P and Q with respect to answer sets (which is the particular case for R is the empty set), and has its applications in program optimization, verification, and modular logic programming. In this paper, we consider more liberal notions of strong equivalence, in which the actual form of R may be syntactically restricted. On the one hand, we consider uniform equivalence, where R is a set of facts rather than a set of rules. This notion, which is well known in the area of deductive databases, is particularly useful for assessing whether programs P and Q are equivalent as components of a logic program which is modularly structured. On the other hand, we consider relativized notions of equivalence, where R ranges over rules over a fixed alphabet, and thus generalize our results to relativized notions of strong and uniform equivalence. For all these notions, we consider disjunctive logic programs in the propositional (ground) case, as well as some restricted classes, provide semantical characterizations and analyze the computational complexity. Our results, which naturally extend to answer set semantics for programs with strong negation, complement the results on strong equivalence of logic programs and pave the way for optimizations in answer set solvers as a tool for input-based problem solving.