平衡理论和答案集程序的推理能力比较

1、平衡理论和答案集程序的推理能力比拟抽象答案集编程（ASP）是人工智能中一种完善的逻辑方法，广泛用于知识表示和解决问题。均衡逻辑将答案集语义扩展到更一般 的程序和理论类。当在ASP中或以更一般的均衡逻辑形式研究理论间关系时，它们通常以答案集的比拟或理论或程序的平衡模 型的形式来理解。强而均匀的等价性及其相对化和投射版本就是这种情况。但是，ASP有许多潜在的应用领域与查询应答相关, 并且根据可以从中推断的内容对程序进行比拟可能很重要。我们制定和研究一些自然等价和蕴涵的概念，用于以推理和查询回 答的方式表达的程序和理论。我们说明，在大多数情况下，这些新的理论间关系与它们的模型理论对应物相吻合。我们还

2、扩展 了以前关于理论和新连接词（称为。水）的投影蕴涵的一些结果。关键字:答案集编程;平衡逻辑;宗教间关系;投射性内涵;ASP中的分叉1.引言答案集编程（ASP）是人工智能中知识表示和解决问题的流行环境。由于高效的答案集求解器，现在该技术在不同领域有 许多应用。均衡逻辑为ASP提供了逻辑基础，并将稳定模型语义扩展到任意命题和一阶理论。它还被证明有助于在答案集语 义下为时间和认识推理生成新的扩展。答案集程序通常用于以模型或答案集的形式提供问题解决方案的一个或多个表示形式。 与Prolog不同，ASP传统上不是被设计为用作查询应答系统。因此，从2开始的对程序之间逻辑关系的研究主要集中在它们的 答案集

3、的比拟上。这就是强和均匀等价的主关系以及它们的相对化和射影版本是如何理解的2, 3, 4, 5o在Datalog域中首先 考虑了强而均匀的等价性6, 7;从那时起，在这方面已经研究了许多非单调形式主义，包括默认逻辑网，因果逻辑9,论证框 架10, 11和基于偏好的形式主义12, 13, 14,仅举儿个例子。强等价性和相关概念的结果己被证明在许多不同的上下文中是 有用的，例如程序简化15或忘记16。但是，查询应答在许多可以应用ASP的域中非常重要。在这种情况下，我们有兴趣比拟不同程序的逻辑结果，例如，看 看他们在回答查询时同意什么条件。这激发了定义和分析以推理和查询答案方式制定的程序之间的等效性

4、和蕴涵关系的挑战。 类似的概念出现在其他基于逻辑的推理系统中。在Datalog中，有一个众所周知的查闻包金概念17。在对本体进行推理的描 述逻辑中，标在.查询不可分割性怛概念（参见例如18）洞样，在抽象论证中，已经研究了纶证宏受方面的强等同性11。在ASP中，如果两个程序具有相同的稳定模型，那么称它们等双;如果它们在添加任何新规那么集下保持等效状态，那么称为 强等或2。如果只能添加新的事实，那么该关系称为一致等价。此外，可以定义强而统一等同的的对空版本，以涵盖新添加的规 那么或事实使用特定语言的情况。投再等价是适当的概念，以防我们对程序的受限子语言的模型等价感兴趣。所有这些关系都在 文献中得到

5、了研究和描述（如上所述）。在19中，还定义了超序N/%的弱和强形式。在这种情况下，我们关心的是理论的相对 强度Q在本文的其余局部，我们基于推理制定了新的理论间和程序间关系，并说明在大多数情况下，它们与众所周知的模型理论 对应物一致。这意味着可以使用熟悉的概念和技术来研究它们。我们始终在非经典逻辑中工作HT这里初那隹，这为均衡逻辑 提供了基础，从而为ASP的稳定模型语义提供了基础。HT在这种情况下特别重要，因为HT模型与理论等价有关.在第2节 中，我们回顾了HT和均衡逻辑，我们为均衡理论定义了三种类型的后果关系。第3节涉及强而统一的等价关系，展示了标准 概念与根据推理公式化的对应概念相比方何。相

6、对化等价的类似程序在第4节中遵循。在第5节中，我们转向理论之间的蕴涵 关系。换句话说，我们从理论的稳定模型和问答能力的角度来处理理论的相对隔至第6节审查投射蕴涵和等价关系;在这里， 我们概括了在以前的工作中获得的一些特征。我们包括标准逻辑程序的投射蕴涵和等价性，并且还涵盖了另外两种情况。一个 引理2.设M为平衡模型（在）和B的子语言.然后,对于任何B公式，.定义11 （8-后果）。为（一） 我们说是比后果之，在符号中，如果对于任何B公式6,.（二）我们说和是比不可分割（对于3）,在符号中如果和.8结果和不可分割性的强版本以明显的方式获得。定义12（强8后果）。为：我们写对于强烈的8-后果）如果

7、对于任何V和B公式（p,.同样适用于强B形别离性:如果对于任何八和B公式,和.相对化版本很容易获得,例如,强8-结果，相对于4 在符号中,当对于A公式和B公式的任何集合口?，.同样,相对于4表示为.我们之前的相对化强等价概念有一个直截了当的投射版本。定义13让和是理论。和起相对于投影到8上的4的强等价，在符号中，如果有的话（空或非空、A公式的集合工，.命题9.两种理论,和,相对于A是强B不可分的,它们相对于/A是强等价的,投影到B上。证明。见附录A. 定义14（强烈的8-蕴涵）。让和是理论。我四说强烈要求相对于4投影到8上，在符号中,如果对于A公式的任何集合强8蕴涵和（相对化）强日后果重合.命

8、题10.对于任何理论，:（3）证明。见附录A. 62理论的分叉和投射B-蕴涵我们已经看到，在均衡模型方面定义的等价和蕴涵概念与以结果或查询回答方式表达的类似对应物之间存在良好的一致 性。正如预期的那样，在（投射）强蕴涵的情况下，该协议与强8-后果的怀疑版本是一致的。对于标准模型理论概念，许多表 征结果是的（参见第8节）。在投射蕴涵和等价的情况下，主要结果是网的结果，它们适用于析取逻辑程序（另见最近的 工作28）。在本文的其余局部，我们考虑了程序和命题理论的投射概念，并利用了分叉的概念。在20中，逻辑程序的语言被扩展为包括一个新的构造。，称为fork,其直观含义是，稳定的模型对应于稳定模型的并集

9、 和在任何上下文中那是.（备注：表示稳定模型的集合.因为一个程序（或理论）在我们的例子中是有限的，我们也可以把它看作 是它公式的结合。这允许我们编写表达式，例如或具有明显的含义）。使用分叉的构造，20研究了分叉的射影强等价（PSE） 的性质：两个分叉满足词汇V的PSE,它们产生相同的稳定模型，投影在V上的任何上方文J匕此属性对应于定义13中为该 案例定义的属性.20还提供了 PSE的语义表征，允许人们证明总是有可能忘记（在强持久性下）分叉中的辅助原子-这在标准 中被证明是错误的.现在，我们回想起19, 20中的一些定义。定义15.鉴于,a厂支持定T的一组子集,即满足iff.为了提高例如的可读性

10、，我们可以将支持编写为方括号之间的一系列解释。例如，可能支持是，或空支撑.众所周知，给定一个命题公式，那么设置：始终是7支撑，表示为.此外，在3中，它说明是一个厂支持iff存在一个命题 公式使得.例如1.如果，我们说一个了支撑是4可行性的没有在满足.（备注：如果，对于某些人来说和，假设是V-不可行的。然后，存 在跟使得.在这种情况下，了永远不会是如果.请注意，和）.引理3（引理7出自20）。鉴于和任何T支撑,有一个命题公式使得和对于任何和.定义16.鉴于,我们说一个下支撑是A尊重，如果有的话跟,因此iff.请注意，当，贝，对于任何，是4尊重。引理4（引理13出自20） o让是两组原子和是一对丁

11、型支撑。然后:（一）（二）止匕夕卜,如果是从尊重，然后我们可以定义7支撑之间的阶次关系 ,方法是说，给定两个丁支撑,和，如果或很明显，和是所有了支撑的类中分别是 底部和顶部元素。回到例如1,很明显，适用于任何.给定7形支撑，我们定义其补充支持如：我们还认为理想的:请注意，空支持不包括在理想中，所以.如果是任何一组支撑：定义亿7型视图定一组T形支撑即金封闭,即.分又是使用以下语法定义的：哪里是一个命题公式，并且是一个原子。对于分叉的7表示法的定义，我们使用隶属关系 的较弱版本，定义如下。给定了视图，我们写潸或两者兼而有之和.定义18（分叉的T指称）。让成为命题签名和一组原子。The厂指称的分叉F

12、,写是一个T视图,递归定义如下:鉴于，概念程序证书在网中用于表征别离程序之间的对应关系。使用指称，我们可以说一对哪里是一组解释和，是一个 程序证书如果存在，以便：或和.是A可行的很容易证明（最小）-程序证书对应于视图的（最大）元素哪里和：在3中，证书用于证明：引理5（引理1来自3）。给定两个别离程序和和两套,它认为：用,对于每个-证书之,那么存在一个-证书之跟.现在，我们可以扩展这个结果，以说明它适用于一般的程序和理论，而不仅仅是别离程序：定理1.给定两个程序,和和两套，我们有:iff,适用于任何.因此，我们还有：定理2.给定两个程序,和和两套，它认为:iff,对于每个63分叉的投射B 蕴涵为

13、了将定义14和定理1扩展到分叉的情况，我们需要一些额外的定义和结果。定义19（定义7出自20）。给定一个分叉F,我们说是一个稳定模型的F （）计f或者,等效地，.定义20.设F和G为分叉和两套。我们说尸强要求G相对于投影到8上的A ,在符号中，如果对于任何叉子L在,.定义21.设F和G为分叉和两套。我们说F和G相对于投影到B上的A非常等价,在符号中，如果对于任何叉子L在. 在20中，说明，如果我们有：定理3.给定F和G两个叉子和,那么以下情况成立:，对于任何,我们从20中回顾，当下是一个分叉时，并且：为了扩展定理3,假设F是一个分叉，和.我们可以定义A视图：以下定理从20中推广定理2 （情况是

14、）因为定理4.给定F和G两个叉子和集合,那么以下情况成立:iff，适用于任何我们需要以下辅助引理来证明上述定理。引理6（引理6来自20） o让是原子的集合,并让L成为一个分支,使得.然后,任何最大在是4尊重。引理7（弓I理18来自20）。让是原子的集合,使得并让F成为一个分叉,使得.然后,对于任何士最大S支持,那么存 在使得.证明（定理4的证明）。见附录A。 推论1.给定F和G的两个叉子和集合以及集合,那么以下关系成立: iff,适用于任何.案例例如：政策推理为了简要说明我们两种宗教关系的实际相关性，让我们考虑一下基于规那么的政然特别是，ASP非常适合表示策略制定 中可能涉及的默认值、典型性和

15、异常。成功采用逻辑方法的一个政策领域是平安和访问控制领域。这个区域已经存在了一段时 间，可以追溯到29。后来的作品包括30, 31, 32, 33, 34。Bonatti 31对该地区进行了调查，并提出了几个可以用Datalog 和答案集编程等语言研究的推理问题。我们松散地遵循他的方法，并在某种程度上扩展它。在访问控制的情况下，让我们假设有一个逻辑程序以一套规那么的形式表达基本政策。假设它可能表达了访问南伍尔弗汉普 顿大学某些受限制网页的条件。此外，还有上下文表达在某些时候成立的其他事实丁也许这个特定的Web区域允许在不同时期进 行不同类型的访问。然后，有凭据这也是（原子）事实。假设，一般来说

16、，只有教职员工才能进入禁区，因此证书可能是.完成 图片，有授权，通常是说明主体是否可以/不能对对象执行操作的陈述，例如，Pedro是否可以访问Web区域。它可能是2值 或3值，具体取决于上下文。使用基于逻辑的语言（如ASP）使我们能够以直接的方式分析可能出现的不同类型的推理问题。正如博纳蒂所观察到的， 最基本的问题是内脑问题。是授权授予者和？如果出现这种情况，其中匕是合适的非单调推理关系，例如关系与稳定的模型语 义相关联。第二个问题实际上是一个诱龙的、滋足的问题。粗略地说，给定授权请求，问题是提供一组条件（凭据），这些条件（凭 据）足以肯定地回答授权，如果存在这样的一组。因此，给定一个集合的数

17、字凭证，绑架问题是找到一个子集给定授权的凭据 和上下文C,使得绑架问题的解决方案可以提供适当的廨释。假设佩德罗最近才加入该学院，但尚未在相应的数据库中注册。他被拒绝访问， 并解释说首先需耍注册过程，即他被告知缺少将授予他访问权限的凭据。第三，存在保守的延伸何题。假设条件已经改变，现在一种新型的用户可能会被接纳，例如，一些学生现在可以访问该区 域，只要他们属于一个特定的委员会。程序被放大为一个新的程序，指定新条件。上下文和凭据集也已放大。但是，我们希 望确保以前有效的所有授权在新形势下继续有效，并且系统中没有产生任何漏洞，从而允许以前被禁止的意外授权。换句话说， 新程序保守期展了前一个程序。第四

18、，还有一个相关的相对掰度祠题。我们可以在给定的上下文中说，策略至少与如果每个授权请求都被接受也被接受. 因此，如果拒绝授权A,那么拒绝授权A为简单起见，让我们暂时抑制上卜文，袈考虑一个政策框架。成为三胞胎哪里是一个理 论，可能以语言中的一组程序规那么的形式存在。，是一组凭据，包括和是授权。让和成为政策框架。然后，我们可以说至少与如 果对于任何和：(4)第五，政策初等性问题可能不同程度。在特定情况下成认完全相同的授权和拒绝的两项政策可以说是等同于该背景下的。 更强的属性是它们在所有上下文中都是等效的。此外，更强大的属性是，当它们通过添加新的策略规那么进行扩展时，它们仍然 是等效的。政策间关系AS

19、P为研究这些推理问题提供了一个合适的框架。除了能够处理牵连、外延、一致性和完整性等问题外，逻辑方法还非 常适合处理上述政策间关系。程序之间的弱和强形式姿脑与捕获（4）所表达的关系相关。例如，获得关系的充分条件是,弱需要 在定义9的意义上。这也意味着该关系在以下情况下成立：强烈要求.然而，为了准确地描述这个概念，我们可以使用相对化统 一蕴含的概念，并考虑对授权的投影。.我们可以说，两个访问策略涵盖相同的凭据和授权，和，如果它们生成相同的授权，那么等舷如果它们被任何新的策略规 那么集扩展时等效，那么为燎等效.如果和是相对化均匀等价物，相对于然后和是强等价的。为了考虑相反的关系，因为我们只需耍 策略

20、来提供相同的授权，所以它们只需耍在投影到.因此，在这种情况下，我们对与投影的均匀或相对化均匀等价感兴趣。.结论我们定义了均衡理论和答案集程序之间的对应关系选择。它们基于理论的推理能力，即它们如何回答查询和推导公式，而 不是基于它们的稳定模型集。这对于ASP的许多应用程序都很重要。特别是，通过包括相对化和投射对应，我们涵盖了 ASP 实际应用中出现的许多情况。不仅理论等同于兴趣，而且理论之间的蕴涵（和结果）关系也是如此。我们己经证明，这些新的关系，包括等价关系和结果关系，实际上在很大程度上等同于过去研究过的稳定和均衡模型所定 义的标准类型的对应关系。在蕴涵关系中不等价或不等价的有限理论和程序可以

21、通过以下类型的查询来区分：在轻信推理的情 况下，文字的连词和在怀疑推理的情况下对文字的析取。这意味着，在ASP中表征理论间关系的大量结果，以及决定这些关系在实践中是否获得的附带技术，直接适用于这 里定义的关系类型。这些结果包括逻辑中程序和理论的强等价性的原始表征2以及从以下方面对均匀等价性的研究模型4, 27和26中的反模型。相对化等价在5和更一般的对应中处理，包括3和28中的投影。沃尔特兰在5中的工作在35中被扩 展为涵盖一般命题理论。有关程序对应关系的进一步工作的广泛参考书目，请特别参见28。在第6节中，我们在两个方面扩展了之前关于射影关系的工作3, 28o首先，在20的基础上，我们应用了

22、厂支持和厂 视图的概念，给出了投射蕴涵和等价的替代特征，这些特征现在扩展到均衡逻辑中的一般命题理论。其次，我们扩展了之前关 于分叉的工作，以产生对分叉之间投射蕴涵的更一般的特征。未来还有许多悬而未决的挑战。例如，这些新的理论间关系如何推广到具有变量的一阶理论和程序的情况下，还有待研究。 一阶理论已经很强的等价性在量化版本中得到了表征在36中，均匀等价在26中处理。最近，37研究了非地面计划等效性的 相对化和投射版本。另一个研究途径是扩展目前的框架，以适应无限的语言和理论。例如，在轻信后果的情况下，在许多情况下，有限查询似 乎会别离非等价理论。考虑公式在引理1 （i）的证明中。在无限理论的情况下

23、，这个公式将成为无限的结合，但对于每个，有 一些从在,所以，如果平衡模型的集合是有限的，我们可以在每个平衡模型中建立一个字面的有限合取false之但在平衡模 型M中为真.因此，有一个有限的查询可以将这两种理论分开。是对任意命题理论的扩展。另一个涉及程序通常词汇表的扩展，以包括一种新型的析取连接词，I 称为分叉，在20中引 入。如第6.2节所述，这种结构的直观含义是，当我们形成稳定的模型时开工| 7T2,它们对应于以下位置的稳定模型的并集 TTI和7T2.当进一步的规那么时，情况仍然如此7T已添加。ASP非常适合正式化基于规那么的弟骼，并且通常人们对给定相关背景信息和数据可以从这些策略中获得的后

24、架感兴趣。 因此，当我们想要以合乎逻辑的方式比拟不同的政策时，我们一直在研究的各种宗教间对应关系是相关的。我们在第7节中包 括了一些段落，这些段落描述了在访问控制策略的情况下，这种策略形式化可能是什么样子的，访问控制策略是过去成功应用 逻辑程序的领域。这个草图可能有助于说明我们的宗教间关系如何为推理这些政策提供有用的概念。有大量的文献致力于答案集程序之间以及平衡逻辑中理论之间的逻辑关系。本文无法描述所有许多表征结果及其应用。但 是，在最后的第8节中，我们列出了一些额外的研究文章，读者可以在其中找到许多最重要的结果。我们将一些较长的证明， 特别是第6节中的证明，移到了附录A中。.逻辑前提和基本定

25、义我们在逻辑中工作HT的这里初那罢首次出现在21中。这是直觉命题逻辑的三值扩展。它可以通过考虑两种真理来以 简单的方式建立：可证明的真理和默认的真理，适用于不假但不可证明为真的命题22。我们还依赖于乎分逻獐，一种非单调性 的扩展HT基于最小模型1的概念。均衡逻辑捕获了任意命题理论的ASP的稳定模型语义。此外HT在研究跨学科关系时 具有很大的价值，因为理论和程序在逻辑上是等价的，当且仅当它们在逻辑上是等价的。HT.语言HT以通常的方式从集合中建立At称为（命题）挣兹阿原子。（命题）公式力使用通常的语法定义： ：二_|_|同忖八例忙/回忖一e其中P是原子At.希腊字母巾，上 丫它们的变体代表公式。

26、我们还考虑派生运算符。二定义（。一，），T二定义_L 和c（p中二定义（巾一中）A （3一巾）.大宇是原子p或其否认理治是一组公式。（一般）皮房是表单的一组含义仇0 哪里a是文字和0文字的析取。别离逻獐程序是一种程序，对于其每个含义a仪0是原子的析放。换句话说，析取程序的 公式恰好具有通常称为逻辑编程题妙的形式，其中a是规那么.万文和0是规那么头。我们用大写的希腊字母表示理论和程序，厂, 7T, 2和At （7T）表示存在于中的原子公式集7T.在整篇文章中，我们将注意力限制在有限的语言，理论和程序上。一种模型理论语义学HT可以基于直觉逻辑的常用可能世界模型（参见例如23）,但是HT帧完整F=W

27、, 4）（其中，像往常一样，w是点或世界的集合，4是w上的偏序）正好有两个世界，比方herd）和丁 CthereD人4七像往常一样, 模型是一个框架和一个赋值/；它与w的每个元素相关联，一组原子,使得如果w4w然后，(w) g(w)然后，赋值通过 直觉逻辑中合取，析取，蕴涵和否认的通常规那么归纳扩展到所有公式，即wwQ e i(w)ikpes中0w4 wQ(w)虽然最后条款是从一和_l的条款中获得的，但我们将其包括在内以明确在任何一个世界都是正确的，以防万一。目(母方便地表示HT模型作为有序对(H/F)原子组，其中H二/(k)和T=i(t)在合适的分配下冲后七因此HH什么时候H=T,我们说解释

28、H/Q是总才。请注意，在模型中(H/0, H表示某些或可证明原子的集合，而丁表示任一类型 的真原子的集合。我们写以表示公式巾在HT型M,即i(w).然后巾在M,在符号中21叫 如果公式巾据 说是理论?结果7T,在符号中7Tu4如果M呐 对于每个模型M之7T.我们表示Tk(M)所有公式的集合真值M.平衡逻辑为了定义均衡逻辑，我们首先引入偏序sonHT模型。定义1.给定任意两个模型，(H JV)人H，我们设置Hn旦H)T)如果丁二千和.这导致了以下平衡的概念。定义2.及n为理论和H/Q n的模型。然后(H.T)据说是一个n的平衡模型如果在n的模型中在m下是最小的,并 且它是全数。换句话说，模型(T

29、/T)之在没有模型时处于平衡状态(H/0之仃跟HU.在这种情况下，我们说7是一个稳定的模型或答案集7T.均衡逻辑是由理论的平衡模型确定的逻辑。我们的术语由以下属性证明：命题1(24) o没F1是一个别离逻辑程序。然后,一组原子T是C的稳定模型(或答案集)(在标准意义上25),当且 仅当T.-Q是n的平衡模型。由于稳定模型语义下的理论或程序通常具有多个稳定或平衡模型，因此可以根据该理论所代表的特定问题域考虑不同的推 理概念。ASP中更常见的关系是怀疑推理;然而，有些应用中，轻信的推理形式更合适。我们还包括第三种类型的声娜断。对于一个理论7T,我们用E(7T)其平衡模型的集合。我们说一个理论TT在

30、以下情况下定原定的E()w0.当很明显我们正在 处理一个平衡模型或任何总体(即经典)模型时21,我们也简单地用它相应的M组(真)原子来表示它。定义3(均衡后果)。均衡后果的关系，轻信(TTm),怀疑(7Tus4),和谨慎(7T叩巾)定义如下。设c为理论。 然后Ftc如果C是稳定的,明gLME(7T)Tk(M);TTz如果c是稳定的,并且 e杂e E(rr)Th(M)7T叩如果n是稳定的,并且 fCM e e()(M)这些关系不同:例如7T= Vb.我们有E(7T)=砂.因此7TM4但不是7Ta也不7T中.此外TTaVb 但7T冷4 Vb一般来说，我们有7T叩色意味着TTus。和TTus意味着7

31、7e.在我们的例如中，7T叩4(因为侏4) 但是7T府4因为.等价概念基于这些关系，我们现在能够定义理论之间不同的等价概念。定义4.让7Tl和IT2是理论和xgqcs)仇然后三oCTYn指出对于任何公式, 7T讣a(piffTTzuacp.我们现在能够以更多不同的方式比拟理论：定义5.让IT，和TTn是理论和X s却4.然后TT1三sTT2对于任何进一步的理论c, (TT，UTT)三(TlaUlT).7Tl三7T2对任何集合X原子的保持iff, (ITi U X)三(7T2 U X).7Tl三saTTz对于左问进一步的理纶n, (TTiU 7T)三a(7T2U 7T). 7Ti=u(xm 对任

32、何集合X原子的保持iff, (TH U X)三0仃2 U X).前两种关系是众所周知的。遵循标准术语，我们说7Tl和172在似下情况下是等效的EQT)=EE4,如果 1T1三S1T2和统一等效顼,如果丁以三，仃2.这些关系是众所周知的。仃1和仃2当且仅当它们在逻辑中等价时，它们才是 强等价的HT；换句话说，它们具有相同的HT型号2。另一方面，均匀等价性由一组特殊的HT反模型26(另见3, 27) o显然，如果理论是等价的，那么它们的推理关系对于所有类型的推理也是等价的。但是，如果两个理论具有不同的平衡模 型，会发生什么情况;我们能不能总是用它们所包含的句子来区分它们？以下引理以肯定轻信和怀疑的

33、推论来回答这个问题。为 了简化符号，我们将平衡模型视为一组原子例。引理1.让和寸2是稳定的理论,使得EQTC)*EQT*;说具有一个平衡模型M,该模型不是F2.然后:(-)有一句,以便Mm但卬在所有平衡模型中都是错误的不2,因此F3c不2求8,等等7T2三口c7T2.(二)有一句话中,以便M押 但Mi叫 对于每个平衡模型MiGEE*.因此 在2号s中 而TT工也中 等等7Ti=Ds7T2.证明。(-)对于 MiE(7T2),我们知道 Mn(UMi)w。或 MiD(UM)，0跟 U=A47TiU7T2).设置然后对于每个/；所以MuQ哪里小二Mi和7T仆涉.但是，对于任何MiE(7T2),Mi绅

34、这意味着7T2 晚 /(二)同样，对于每个均衡模型Mi之7T2要么有一些原子使得M止4否那么有一些原子。金UM使得M*b,其中U是TTtUTTz.设置i=/a e Mn(UMD4 V /b e然后中二在每个平衡模型中的保持172.等等7T2tsy通过检验2!科 等等7Tl应y口 现在，描述蕴涵等价性非常简单。命题2.以下条件成立:TT亡 cTTziffTT工三 s7T2/ffE（7Ti）= E（7T2）.7Tx=（x7Tz 意味着TT工三plT2 为0（。，.接下来的结果说明，在强等价设置中，结果算子的选择不起作用。结合上面的观察，我们得出结论，所有这三个概念都以 这里和那里的逻辑为特征。命题

35、3.以下命题是等价的:（一）7Tl 三 s7T2 /（二）7Tl三 sc7T2 ；（三）7T 三 ssTTa ；（四）TT1三spTT2证明。（第（一）-（三）局部）显然，（一）意味着（二）和（三）。但是，如果（i）不成立，那么就有一个理论。7T使得（10），（7?2口77）-应用引理1得出两者都不开1三6。九2也不开1三ssTT2保存。TT工mTT2TTT,E（TT工 U 7T）二E（7T2 U TT）UTT,TT，U 7T三c7T2 U 7T中工三scTT2mTE（TT工 U TT）二E（TT2 U 7T）nTTjTTi U 7T 三 sTT2 U 7T qT i 三ssTTzbgProp

36、ositi。八2 bgp匕。？。5才/。八2证明（TTi三sTTzTT工三spTTa只要说明7Tl三spTTzTTn三sTTz.假设7Tl三Els7T2.因此，存在一个7T使得(TTi U 7T)三口772 U 7T).通过命题2,我们可以假设Y EfTTi U TT)E(TT2 U 77)考虑TT=用 e八 & UYn其中u是出现在 mumu 丁r那么，v是唯一的平衡模型 muTTu rr而e（tt2 u ttu tt）=。.这可以看作如下。唯一 HT型号TT形式均为（X/Y）跟乂，因为没有X4是一个HT-模型7T1U7T （按假设Ye E（TU U 7。），否X4是一个HT-模型771口7

37、7日77因此，V是唯一的平衡模型7T工U 7TU 7T.另一方面，从假设Y在（7T2U TT） 我们可以有两种情况：（一）（丫不是HT-模型7T2UTT.那么，V显然不能成为TT2U7TU7T或（二）（丫是一个HT-模型7T2U7T但后来存在X4使得（X，X）是一个模型TT2UTT.根据定义m（X,Y）然后也是一个模型TTurTUTT,因此 Y不能是 7TU TTU 7T.然后，我们可以得出结论：YWEaTzUTTUTT）并且，因为丫是唯一的经典（总）模型TTzUTTUTR因此E（7T2U 7TU TF）= 0.现在，利用以下事实：具有独特的平衡模型，显然存在一个（非重言式）使得和.因此.口请

38、注意，此参数也适用于析取逻辑程序（使用约束）。均匀等效性对于持怀疑态度和轻信的案件，统一等同的情况恰恰遵循了以前的模式。命题4.以下条件是等价的:（-）（二）证明。对于谨慎的情况，考虑空理论和包含公式的理论.这两种理论并不统一等同。事实上，它们甚至通常不等价，因为前者具 有独特的稳定模型0而后者具有两个稳定模型。和.请注意，在这两种情况下，所有稳定模型的交集解是0,因此它们通常等效于 谨慎查询。此外，如果我们在这些理论中加入上下文，我们会得到相同的稳定模型。，和.因此，对于谨慎的后果，它们也是统一 等价的。.相对化等效像往常一样，我们考虑理论，等，现在制作显式语言，等。和以前-一样，我们将语言视为一组原子。理论据说在语言中如果 它的所有原子公式都属于.定义6.让和是理论。