A General Framework for Equivalences in Answer-Set Programming by
  Countermodels in the Logic of Here-and-There
  Different notions of equivalence, such as the prominent notions of strong and
uniform equivalence, have been studied in Answer-Set Programming, mainly for
the purpose of identifying programs that can serve as substitutes without
altering the semantics, for instance in program optimization. Such semantic
comparisons are usually characterized by various selections of models in the
logic of Here-and-There (HT). For uniform equivalence however, correct
characterizations in terms of HT-models can only be obtained for finite
theories, respectively programs. In this article, we show that a selection of
countermodels in HT captures uniform equivalence also for infinite theories.
This result is turned into coherent characterizations of the different notions
of equivalence by countermodels, as well as by a mixture of HT-models and
countermodels (so-called equivalence interpretations). Moreover, we generalize
the so-called notion of relativized hyperequivalence for programs to
propositional theories, and apply the same methodology in order to obtain a
semantic characterization which is amenable to infinite settings. This allows
for a lifting of the results to first-order theories under a very general
semantics given in terms of a quantified version of HT. We thus obtain a
general framework for the study of various notions of equivalence for theories
under answer-set semantics. Moreover, we prove an expedient property that
allows for a simplified treatment of extended signatures, and provide further
results for non-ground logic programs. In particular, uniform equivalence
coincides under open and ordinary answer-set semantics, and for finite
non-ground programs under these semantics, also the usual characterization of
uniform equivalence in terms of maximal and total HT-models of the grounding is
correct, even for infinite domains, when corresponding ground programs are
infinite.
