摘要翻译：
在答案集规划中，人们研究了不同的等价概念，如强等价和一致等价等，主要是为了识别在不改变语义的情况下可以作为替代的程序，例如在程序优化中。这种语义比较通常以这里和那里(HT)逻辑中的各种模型选择为特征。然而，对于一致等价性，用HT模型进行的正确刻划只能对有限的理论和程序进行。在这篇文章中，我们证明了HT中的一个反向模型的选择对于无穷大的理论也是一致等价的。这一结果被反模型以及HT模型和反模型的混合（所谓的等价解释）转化为不同等价概念的一致表征。此外，我们将程序的关系化超等价的概念推广到命题理论中，并应用同样的方法，以获得一个可适应无限设置的语义刻画。这允许将结果提升到根据HT的量化版本给出的非常一般的语义下的一阶理论。因此，我们得到了一个研究回答集语义下各种理论等价性概念的一般框架。此外，我们证明了一个方便的性质，允许简化处理扩展签名，并为非基础逻辑程序提供了进一步的结果。特别地，在开放和普通回答集语义下一致等价是一致的，对于在这些语义下的有限非接地程序，即使对于无限域，当相应的接地程序是无限的时，通常用接地的最大和总HT-模型来刻画一致等价也是正确的。
---
英文标题：
《A General Framework for Equivalences in Answer-Set Programming by
  Countermodels in the Logic of Here-and-There》
---
作者：
Michael Fink
---
最新提交年份：
2010
---
分类信息：

一级分类：Computer Science        计算机科学
二级分类：Artificial Intelligence        人工智能
分类描述：Covers all areas of AI except Vision, Robotics, Machine Learning, Multiagent Systems, and Computation and Language (Natural Language Processing), which have separate subject areas. In particular, includes Expert Systems, Theorem Proving (although this may overlap with Logic in Computer Science), Knowledge Representation, Planning, and Uncertainty in AI. Roughly includes material in ACM Subject Classes I.2.0, I.2.1, I.2.3, I.2.4, I.2.8, and I.2.11.
涵盖了人工智能的所有领域，除了视觉、机器人、机器学习、多智能体系统以及计算和语言（自然语言处理），这些领域有独立的学科领域。特别地，包括专家系统，定理证明（尽管这可能与计算机科学中的逻辑重叠），知识表示，规划，和人工智能中的不确定性。大致包括ACM学科类I.2.0、I.2.1、I.2.3、I.2.4、I.2.8和I.2.11中的材料。
--

---
英文摘要：
  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.
---
PDF链接：
https://arxiv.org/pdf/1006.3021