Synonymous theories in answer set programming and equilibrium logic

The study of strong equivalence between logic programs or nonmonotonic theories under answer set semantics, begun in [18], is extended to the case where the programs or theories concerned are formulated in different languages. We suggest that theories in different languages be considered equivalent in the strong sense or synonymous if and only if each is bijectively interpretable (hence translatable) into the other. Since the logic of here-and-there, which provides a suitable foundation for answer set programming, has the Beth property, we can easily give model-theoretic conditions that are equivalent to bijective interpretability. These conditions involve mappings between the models of the two theories that, in particular, preserve the property of being an answer set or equilibrium model.