毕业设计（论文）文献译文：强等价逻辑编程

毕业设计（论文）--文献翻译原文题目StronglyEquivalentLogicPrograms译文题目强等价逻辑专业信息与计算科学姓名学号指导教师强等价逻辑编程VLADIMIRLIFSCHITZUniversityofTexasDAVIDPEARCEEuropeanCommissionandAGUSTINVALVERDEUniversityofMalaga摘要逻辑程序Π1被认为等价于在答案集上的逻辑程序Π2，如果Π1和Π2具有相同的答案集的语义。对于每个逻辑程序Π，Π1Π和Π2Π具有相同的答案集。研究强等价性很重要，因为我们从中学到了如何简化逻辑的一部分程序，但还并不完善。主要定理表明，验证强等价性可以通过检查单调逻辑中公式的等价性来实现，此处的逻辑是古典逻辑和直觉主义之间的逻辑。类别和主题描述符：F.4.1[数学逻辑]：逻辑编程逻辑编程一般条款：语言，理论附加关键词和短语：答案集，逻辑编程，稳定模型

4.3直觉逻辑论程序的例子（4）和（5）表明，在这两处中逻辑定理1的陈述不能被直觉逻辑所取代：这些程序是强等价，但不直观的等效。程序（4）在语法上是相当复杂的：它包含一个析取规则和约束。但我们可以给出一个类似的反例不使用规则这些。如下程序q←notpp←notqr←p,q(12)s←ps←q通过添加规则获得（12）的程序s←notr(13)可以证明使用克里普克模型这些项目并不是互相等效的直观的。但它们是强等价的。从获得的r→sp→qq→p(p∧q)→r(14)p→sq→s在HT，假设R使用公式第三（14）和德摩根定律，我们得到p∨q.：使用第一个公式（14），我们得到的p∨q问：使用最后两个公式（14），我们推导出s。4.4平衡逻辑为证明主要定理，我们将利用一些结果非单调推理称为平衡逻辑。平衡逻辑可以描述为HT逻辑中的一种特殊的最小模型推理，理论0的均衡模型是一个整体HT，如下考虑，例如，理论包括一个单一的原子公式p.其模型在逻辑HT上是<{p},{p}><{p},{p,q}><{p,q},{p,q}>首先是均衡模型。第二个不是，因为它不是完整的。第三也不是均衡模型，因为它不满足最小条件（II）。另一个例子是，这个模型属于HT逻辑：<,{p}><{p},{p}>这也不是均衡模型：第一个它不完整，第二个不是最小。事实上，这一理论没有均衡模型。引理1。对于任何没有失败的程序，都是一个HT模型<IH,IT>。而在HT模型中得到解释，在HT模型上，Head←Body是一个经典模型。<IH,IT,H>|=Bodyimplies<IH,IT,H>|=Head <IH,IT,T>|=Bodyimplies<IH,IT,T>|=Head因为不包含否定，这些条件可以简化如下：IH|=BodyimpliesIH|=HeadIT|=BodyimpliesIT|=Head为每一条规则要求head←body这个规则，也就是要求其在古典逻辑的意义上是以上模型。引理2。一个HT解释下符合<IH,IT>，那么它产生于。引理的证明使用了两个可以很容易通过结构进行验证的事实归纳。一是对“单调性”的解释:例1对任何HT解释法下的<IH,IT>和任何命题公式F，如果<IH,IT,H>|=F然后<IH,IT,T>|=F。另一种则关系到HT满意度关系的古典逻辑:例2对于任何HT解释下的<IH,IT>和任何命题公式F，如果<IH,IT,T>|=F那么IT|=F.证明引理2。根据还原(第3部分)的定义，是由同时替换一些的程序获得的程序最大的子公式形式不是⊥相关的F，和所有其他与⊥相关形式。它有足够的自检性，对于任何最大值子公式，notF可以替换它的公式G，<IH,IT>|=notFiff<IH,IT>|=G由于G不是⊥，也可写作<IH,IT>|=notFiffG=⊥这个等价的左边是iff<IH,IT,H>|≠Fand<IH,IT,T>|≠F结合实例1，第一项就是第二项的结论，所以也可以被删除。结合实例2，第二项可以写为IT|≠F,它是G=⊥的条件。因为<IT,IT>满足每一个公式,它是一个∪的模型。可以看出它处于平衡状态,在考察任何模型时<J,IT>，∪是IT子集。显然J必须包含IT。但它不能等于IH，因为假设<IH，IT>，H⊂J⊂T。用一个原子A∈J\IH和原子B∈IT\J.这些原子，A→B属于。但<J,IT>不满足这个含义，与它是a的假设相反。最后，可证<IH，IT>不是一个平衡模型。因此，T的任何一个合适的子集，都不是一个均衡模型∪。

五．增加第二否定答案集通常定义为具有第二种类型的逻辑程序否定，表示一个原子的直接或明确的否定。在gelfond以及Lifschitz[1991]和Lifschitzetal.[1999]，这第二个否定被称为“古典”,可以理解是命题原子或原子前缀。我们定义扩展公式、扩展规则和扩展程序我们在上面的第3部分中定义了公式、规则和程序，任意的字符可以代替原子。语义扩展程序定义的是一个一致的集合X是一个答案集扩展程序，详细信息见Lifschitzetal.[1999]。对逻辑程序的语法添加第二个否定是很重要的。但在实际应用上，计算上，这个扩展并不是很重要。事实上，第二个否定可以通过一个简单的语法转换从程序中消除。对每个原子A的基础语言，选择一个新的原子。例如，如果是p;pq←p(15)q是p;q←p(16)⊥←p,⊥←q,(假设底层语言中除了p和q之外没有原子)只有答案集(15){p};因此,唯一的答案由(16)得{}。关于程序的强等价性的问题也出现在这个问题上扩展问题。例如，它在Erdem和Lifschitz(1999)中显示，在任何扩展程序中，分隔规则p;p(17)可以等价地用两个非分隔规则替代p←notp¬p←notp(18)下面的定理允许我们减少对扩展程序的强等价性的验证，以检查公式的HT等价性。例如，要看，(17)和(18)就足够检查HT的等效性图1所示。逻辑程序语言与命题语言之间的对应关系存在两个否定的公式。p←not←notp⊥←p,但这些都是在介绍中讨论过的项目(4)和(5)代替q，重写为一组命题公式，这两个程序变成(6)和(7)，在第二节，我们已经证明了它是等价的。命题公式识别公式和规则延伸它们,我们可以把第二否定写作∼。在之间的对应了关系逻辑程序的语言和命题公式的语言，图1总结了两个否定的存在。我们的主要定理很容易概括为新的设置(证明的方法是完全相同的)，我们可以证明两个扩展的程序是强等价的，当且仅当它们在逻辑N5中是等价的。有趣的是，从本节开始讨论的扩展程序中消除第二个否定的方法可以推广到N5。对于N5语言中的任何公式F，都有一个相当于“减少”的公式r(F)的第二否定象征∼，这样它就可以直接站在一个原子的前面[Vorob'ev1964]。考虑一下消除第二否定的句法转换，公式F通过替换每个部分的形式∼r(F)和一个新的原子的形式。这类似于由古雷维奇(1977年)提出的直觉逻辑Nelson强烈否定的逻辑。

6结论有关逻辑程序的强等价性的事实告诉我们，如何在不查看其他部分的情况下简化逻辑程序的一部分。强等价性可以用各种各样的逻辑来描述。这一逻辑的理论集合包括所有直观的可命题公式，被排除的中间弱法则，以及德摩根的定律。两个程序是强等价的这一事实通常可以通过推导得到彼此使用这些逻辑方法。这里有一个指数时间算法用来验证强等价。Reiter和Gelfond的扩展的非分隔程序的定义是：这一观点认为，这些程序只不过是Gelfond的默认理论的一个特例。默认值是推理规则的泛化：除了前提和结论，违约有“理由”。因此，逻辑符号←是程序类似于将结论与前提相分离的方法推理规则。在