多Agent自认知逻辑的逻辑程序化

54理论计算机科学电子笔记70第5期（2002）网址：http://www.elsevier.nl/locate/entcs/volume70.html18页多Agent自认知逻辑的逻辑程序化TOYAMA，Katsuhikoa，b，1，KOJIMA，Takahiroa，和稻垣康吉a，2a名古屋大学工学研究生院，日本名古屋464-8603，千草区，b名古屋大学综合声学信息研究中心，日本名古屋464-8603，千草区，摘要为了开发多主体自认知逻辑（MAEL）的证明过程， 一个自然的框架，形式化的信念和推理，包括继承，持久性和因果关系，我们介绍了一种方法，翻译的MAEL理论到一个逻辑程序的完整性约束。本文证明了MAEL理论的扩展与由其翻译的逻辑程序的稳定模型之间存在一一对应关系，并证明了这种方法的优点：（1）只要计算翻译后的逻辑程序的所有稳定模型，就可以得到MAEL理论的所有扩展。(2)我们可以充分利用有效的技术或系统来计算逻辑程序的稳定模型。我们还调查了属性的推理MAEL通过这种翻译。可拓计算问题可以归结为稳定模型计算问题，这一事实意味着MAEL与非单调推理的其他形式化之间有着密切的关系。1介绍众所周知，当我们用非单调逻辑形式化信念时，会同时出现一些困难的问题，如多延拓问题[3，17]和时间投影问题[5]。作为一种在形式逻辑框架中处理此类问题的方法，已经提出了多智能体自认知逻辑（MAEL）[19]MAEL是1电子邮件：toyama@nuie.nagoya-u.ac.jp2电子邮件地址：inagaki@nuie.nagoya-u.ac.jp2002年由ElsevierScienceB出版。 诉 操作访问根据C CB Y-NC-N D许可证进行。大沼、小岛和永木55通过将自动认知逻辑（AEL）[13]扩展到具有多模态和多理论的逻辑来形式化，其中代理之间的信念获取关系及其优先级可以通过公式来指定。因此，MAEL是一个非常容易理解的框架，我们可以自然地表示信念和推理，包括继承、持久性和因果关系[19]。由于需要实现基于MAEL的信念处理系统，因此需要开发一种有效的定理证明过程（理论扩展的计算方法）文[6，7]中提出的方法是基于tableau方法结合归结原理。然而，该方法只判断由初始信念集导出的推理结果中是否包含给定公式，不容易得到完整的推理结果推理（什么和多少结果集来自初始信念集）。因此，研究一种新的MAEL证明方法，使其能够得到所有的推理结果，是MAEL的一个基本问题，阐明MAEL的推理性质为了对基于不完全信念或常识知识的推理系统进行建模，迄今为止已经提出了以下非单调推理的形式化：缺省逻辑、NML、AEL和限定、逻辑编程、真值维护系统（TMS）和溯因等。虽然这些形式化是从不同的背景和动机提出的，各种研究表明，它们之间有着密切的关系[2，4，8，9，11，12，14]。特别地，建立了作为逻辑程序的声明语义的稳定模型语义[4]通过在AEL中应用理论稳定性的概念。Gelfond[4]证明了具有稳定模型语义的逻辑程序可以被看作是一个有限制语法的AEL理论。这意味着一个逻辑程序可以通过转换成一个AEL理论在本文中，我们证明了逆变换到Gelfond将AEL理论转化为具有稳定模型语义的逻辑程序，并且这种转化可以扩展到多智能体系统，即，梅尔。鉴于实现基于MAEL的推理系统的目标，该翻译在以下两点上是重要的• 这种翻译可以作为一个新的定理证明过程MAEL。本文给出了将MAEL理论转化为逻辑程序的具体方法，保证了转化前后推理结果的一一对应因此，只要将MAEL理论转化为逻辑程序，并计算其稳定模型，就可以得到该理论的推广。这表明在MAEL的定理证明中可以直接利用已有的稳定模型计算的研究成果和系统。而且，只要计算出翻译后的逻辑程序的所有稳定模型，大沼、小岛和永木56• 这个翻译清楚地表明，两个不同的形式化的非单调推理，MAEL和逻辑编程，是密切相关的。本文的结果表明，MAEL可以用逻辑程序来描述，这是一个更简单的形式化的非单调推理，如果翻译规则描述得当。当我们研究MAEL形式化推理的性质时，从一个更简单的形式化来理解MAEL的尝试是有用的。此外，这表明逻辑编程作为一种基本的语言，描述非单调推理系统的多代理的可能性。为了实现这种翻译，需要解决以下两个问题：• 如何将MAEL理论扩展到描述多智能体系统，并将其转化为单个智能体的理论，以及如何在逻辑程序中得到相应的• 如何用逻辑程序的规则描述MAEL中形式化的每个Agent在本文中，我们表明，这些问题得到解决，并从MAEL理论翻译成逻辑程序是可能的。论文的其余部分组织如下：第2节概述了MAEL的定义和表征。给出了逻辑程序的定义，包括完整性约束和稳定模型语义。在第3节中，定义了一个称为扩张基的不动点，它表征了MAEL理论的扩张。如果一个理论是一个有限集，那么扩张基将是一个有限不动点集。第四节介绍了如何将MAEL理论转化为包含完整性约束的逻辑程序。翻译前后的推理结果（扩展和稳定模型）具有一一对应的关系。在第五节中，我们讨论了MAEL中推理的性质以及与前人研究的关系。第六部分是本文的结论。2预赛2.1多Agent自认知逻辑MAEL[19]是多智能体系统的非单调逻辑，并通过将AEL[13]扩展到多模态和多理论的形式化。它刻画了多智能体系统中智能体通过命题推理和自认知推理所能获得的信念状态。由命题公式集L0和模态算子集Li（i=1，…，n）以通常的方式。 公式Li p表示代理i具有信念p（或代理i相信p）的Meta信念。一个理论是一个n元组T =（T1，...， Tn），其中Ti表示以下的信念集合：大沼、小岛和永木57||||代理岛在MAEL中形式化的Agent被假设为在逻辑推理和自认知推理能力上是理想的，如下所示：• 逻辑推理能力：每个智能体在逻辑上是无所不知的，他的信念在命题逻辑推理下是封闭的• 自动认知推理能力：从代理获取的信念是根据多代理系统中的自动认知推理形式化的，即，如果代理i具有信念p，则每个代理可以获得Meta信念Li p，并且如果代理i不具有信念p，则每个代理可以获得元信念Lip。如果给定每个主体的初始信念状态，MAEL刻画了由命题逻辑推理和自认识推理得到的最终信念状态（理论的扩展定义2.1序数原子公式是L 0中的命题变量。模态原子公式是形式Li p的公式，其中p是公式。原子公式是序数原子公式或模态原子公式。原子公式和它们的反式称为文字。定义2.2命题解释I是对公式真值的一种通常赋值。如果I对一个公式p赋值为真，我们记为I=p。将真赋值给公式集合Pi的每个元素的命题解释是Pi的命题模型。由于模态原子公式Li p在命题解释中被视为一个新的命题变量，因此它的真值不依赖于p的值。因此，我们定义了一种解释，它反映了李普的意图。定义2.3关于理论T =（T1，...， T n）是一个命题解释I，它满足我|= L i p ip ∈ T i （i = 1，.， n）的对于任何公式P。一个关于T的自认识解释，它给一组公式Pi的每个元素赋值为真，是Pi关于T的自认识模型。接下来，我们根据自表模型定义一个逻辑结果关系=T定义2.4设P i是一组公式，T =（T1，...，n）是一个理论。然后，对于公式p，Pi=Tp，如果对于Pi关于T的任何自认识模型I，I=p。我们定义了一个理论的扩展，它被认为是MAEL中的推理结果（一组定理）。大沼、小岛和永木58∈ ¬∈定义2.5设P =（P1，...，P n）是一个理论。理论T =（T1，...，（1）满足Ti={q∈Lmael|Pi|=Tq}（i=1， . ，n）是P的扩张。从这个定义出发，一个理论一般可以有0个或多个扩张定义2.6理论T=（T1，.，Tn）是稳定的，如果它满足以下条件（1）-（3），对于任何i（i = 1，...，n）：(1) Ti在命题推论下是闭的。(2) 若p∈Ti，则对任意j（j = 1，.，n）。(3) I f p∈Ti，对于一个yj（j=1， . ，n）。众所周知，理论的推广是稳定的[19]。2.2基于MAEL的知识表示作为MAEL的一个应用，在[19]中提出了一种表示知识继承的方法，其中分类层次中的一类知识被视为智能体。当代理i的信念从代理j的信念继承时，LjpL i p被赋予代理i的初始信念集合Pi，其中p是要被继承的信念我们可以这样理解这个公式：如果代理i既获得代理j有信念p的Meta信念，又获得代理i没有任何与p不一致的信念的元信念，那么代理i可以获得信念p。例2.7考虑下面的信念（“尼克松钻石”），它产生了属性的多重继承：“贵格会教徒是和平主义者。"这些信念可以用MAEL来表示。让代理1，2，3分别是贵格会，共和党和尼克松的属性持有者。然后，作为代理的初始信念状态，我们描述理论P=（P1，P2，P3）如下：P1={ Pacifist}，P2={<$ Pacifist}，P3={L1p<$$>L3<$p<$p，L2p<$$>L3<$p<$p}，其中p是任意公式。P3中的公式表明尼克松继承了贵格会和共和党的双重属性。理论P有两个扩展，T =（T1，T2，T3）和TJ=（T1J，T2J，T3J），其中PacifistT3，而PacifistT3J。也就是说，我们可以得到两个推理结果因此，通过使用MAEL，我们可以表示信念，以便两个或更多个大沼、小岛和永木59∈L当关于代理之间的推理的竞争出现时，可以在不使理论矛盾的情况下获得推理结果。2.3MAEL的正规形式我们证明了MAEL的任何公式都可以转化为小句形式和范式。定义2.8下列形式的公式为子句形式。L1a1，1.. . L1a1，l（1）. L1b1，m（1）. ∧一个一个，一个. . . . Lna1，l（n）. Lnbn，m（n）其中ai，j，bi，j，c0，以及先行词中的合取词的每个元素可以不存在。 一个理论是一组子句形式公式的n元组，也称为子句形式。下一个定理[16]给出了一个将任何公式转换成子句形式的算法，即通过从左到右方向重复地将（1）定理2.9对于关于任何稳定理论T =（T1，...，T n），则对于任何公式p、q，以下等价（1）-（7）成立：(1) 我|= L i（p <$q）i <$I |= L i p L i q，(2) 我|= L i L i piI |= L i p，(3) 我|= L j L i piI| = L i p <$L j<$ （i/= j），(4) 我|= L j<$L i pi I |=<$L ip L j，(5) 我|= L i（L i p q） iI |= L i p L i q，(6) 我|= L j（L i p <$q）i <$I |= L i p <$L j q<$L j <$（i/= j），(7) 我|= L j（<$L i p <$q）i <$I |=<$L i p <$L j q <$L j <$，其中，k是表示不一致性的特殊变量。注意，即使i=j，（4）和（7）也成立。这一翻译如图所示其中P、Q、R是命题变量。通过这种翻译获得其要素的理论是小句形式的。Ogawa[16]从理论的扩张是稳定的这一事实以及通过翻译证明公式等价的上述定理证明了我们可以将任何理论翻译成子句形式而不改变其扩张。定义2.10下列形式的公式是标准形式：L1a1L1b1，1.. . L1b1，m（1）. Lnan .Lnbn，m（n）大沼、小岛和永木60∈L∧∧L1（（L2PQ）L1P）R↓L1（（L2PL1P）（QL1P））R↓（L1（L2PL1P）L1（<$L1PQ））R↓（（L2PL1<$L1PL1）（<$L1PL1QL1））R↓（（L2P<$L1PL1L 1）（<$L1PL1QL1））R↓（L2P<$L1PL1 R）（<$L1PL1QL1R）↓（L1P<$L1<$L2PR）（L1P<$L1Q<$L1R）图1.一、翻译成从句形式的例子其中ai，bi，j，c0，以及先行词中的连接词的每个元素可以不存在。一个理论如果是一个正规形公式集合的n元组，也称为正规形理论。再由定理2.9（1），我们可以将子公式L i a i，1<$. 将Liai，l（i）与Li（ai，1）以小句形式进行组合.... . . 你 好 。 .ai，l（i）），从而证明了任何子句形式公式都存在一个等价的范式.因此，我们可以立即得到下面的定理，这是[11]中结果在多智能体情况定理2.11任何理论都可以在不改变其扩张的情况下转化为规范型理论.请注意，模态算子的任何嵌套都不会出现在范式公式中。因此，我们可以在不改变其含义的情况下删除它们。在下文中，我们假设一个理论是标准形式的。2.4逻辑程序在本节中，我们定义了一个具有完整性约束的逻辑程序的稳定模型，与[18]相同。我们假设程序规则中出现的所有变量都是接地的。定义2.12设A i（i = 0，...，n）是原子。逻辑程序是一组大沼、小岛和永木61≤≤LL形式的程序规则a0级←A1，.，A m，不是A m+1，...，不，不;其中0m n. A0是规则的头，A1，.，A m，不是A m+1，...，notA n是它的身体定义2.13完整性约束是一个程序规则，其中头部是一个特殊的原子假，表示不相干。定义2.14设P是具有完整性约束的逻辑程序。P的稳定模型是满足以下条件（1）和（2）的原子集合S：(1)S与reduce（P，S）的最小模型一致，reduce（P，S）是通过以下过程（a）和（b）从P获得的定义逻辑程序。(a) 删除所有规则，使得{A m+1，...，A n}S/= from P.(b) 删除所有非A m+1，...，而不是从其余规则的主体中删除。(2) false∈/S。13扩展基板在本节中，我们定义了一个表征理论扩展的不动点，其中理论中的模态算子所引用的公式起着重要的作用。定义3.1设P =（P1，...， P n）是一个正规形式理论。 一个理论LP=（LP1，...， LPn），定义如下，是P的测试域：LPi={q|LiqoccursinnPj}（i= 1，.，n）。j=1由于P中的公式被假定为标准形式，LPi<$L0。从这个定义出发，如果一个理论P由有限组公式组成P也是有限的。接下来，对于规范型理论，我们定义一个固定点，它是它的测试域的子集。定义3.2设P =（ P1，...，Pn）是一个正规形理论，且LP=（ P1，.，Pn）是P的一个测试域。 则理论B =（B1，.，B n）这样 的Bi={q∈LPi|Pi|=Bq}（i=1， . ，n）是P的扩张基。1条件（2）如果我们加上“奇循环”就可以删除。false′←不是fal s e′，是false。这里false′是一个原子，在其它规则中不发生任何事情。大沼、小岛和永木62LL定理3.3设P=（P1，…，Pn）是正规形理论且LP=（P1，...，Pn）是P的一个测试域，则P的扩张与扩张基之间存在一一对应。 扩展T =（T1，...，Tn）和扩展基B =（B1，.，B n）满足Ti ∈ LPi=B i（i= 1，.， n）。这个定理表明，理论的扩张可以用理论中模态算子所涉及的公式是否属于它的扩张的条件来刻画。例3.4再次考虑例2.7为了成为一个理论P，一个有限公式集的三元组，我们限制了要继承的属性如下：P1={ Pacifist}，P2={<$ Pacifist}，P3={L1 Pacifist L 3L3 Pacifist Pacifist}。和例2.7一样，P=（P1，P2，P3）有两个扩展.P的测试域是LP=（LP1，LP2，LP3）=（{Pacifist}，{Pacifist}）。的情况下B=（B1，B2，B3）=（{Pacifist}，{ Pacifist}），B是P的扩张基，因为{q∈LP1|P1|=Bq}={Pacifis t}=B1，{q∈LP2|P2|=Bq}={<$Pacifis t}=B2，{q∈LP3|P3|=Bq}={Pacifis t}=B3.同样，B J=（B1J，B2J，B3J）=（{Pacifist}，{<$ Pacifist}，{<$ Pacifist}）也是P的扩张基。4MAEL到逻辑程序在这一节中，我们展示了一种将范式理论转化为逻辑程序的方法。我们可以从这个翻译后的逻辑程序中计算可拓基。大沼、小岛和永木63¬定义4.1对于规范型理论P =（P1，...，P n），tr（P）是一个逻辑程序，它由下列翻译规则（1）-（3）产生的程序规则组成：(1)对于任意i（i = 1，.，n），如果然后L1a1L1b1，1.. . L1b1，m（1）. ∧LnannLnbn，1.. . <$$>Lnbn，m（n）<$c∈Pi，fact（i，c）←be l（1，a1），notbe l（1，b1，1）， . ，不是l（1，b1，m（1））， . 、是l（n，ann），不是l（n，bn，1）， . ，n不是l（n，bn，m（n））。∈tr（P）.(2) F或a nyi（i=1， . ，n），若p∈LPi且Q={q1， . . . ，qk}是C P i的极小子集使得（P i<$L0）<$Q|= p，fact（i，p）←fact（i，q1），.，fact（i，q k）.∈tr（P），哪里CPi={c|L1a1.. . <$$>Lnbn，m（n）<$c∈（Pi−L0）}.(3)对于任意i（i= 1，.，n），若p∈ LPi，则bel（i，p）← not not bel（i，p）. notbel（i，p）← not bel（i，p）.n∈tr（P）.false← bel（i，p），not fact（i，p）.false←nottbe l（i，p），fact（i，p）.我们解释了每种类型的程序规则的含义(1) 是从代理i相信的信念或推理规则转换的程序规则。此时，新的谓词bel、not bel和fact被引入到逻辑程序中，并且Li p和Li p形式的文字分别被bel（i，p）和not bel（i，p）替换。一个不包含模态算子的序数原子公式p被替换为原子事实（i，p），如果p出现在Pi中。(2) 是一种程序规则，用于赋予逻辑程序逻辑蕴涵的能力，因为代理被假定为逻辑全知。逻辑程序中的程序规则只能在从右到左的方向上使用，因此，需要将逻辑结果关系清晰地描述为规则。然而，由于它是困难的，以描述所有的关系，我们只描述所需的部分计算的扩展基地。当验证是否满足定义3.2中的条件时，测试域LP中的公式是否是从每个代理的初始大沼、小岛和永木64LLL|∈¬¬信仰是需要的。因此，对于任何代理i（i= 1，.，n），只需要描述LPi中公式从初始信念Pi <$L0和可能新得到的信念CPi的命题可导性规则.(3) 是一种程序规则，用于赋予逻辑程序自动认知推理的能力（3）的前两条规则描述了谓词bel和not bel的性质，它们将稳定模型分为bel（i，p）成立的模型和not bel（i，p）成立的模型。这对应于Li p和<$Li p的文字之一对MAEL中的任何代理i由于这些规则是为测试域P中的任何公式生成的，因此我们可以考虑考虑所有关于每个代理是否具有公式的信念状态，P是他的信仰。这种穷举性保证了我们可以从稳定模型中获得所有的可拓基（完备性）。（3）的最后两个规则是完整性约束，其描述事实（i，p）必须在bel（i，p）成立的模型中成立，而事实（i，p）不必在bel（i，p）不成立的模型中成立这些约束的预期含义是关于代理人的信念的以下内容：代理人i可以通过某种推理从他的初始信念导出信念p（P i| = Bp），并且如果有一个信念p（p∈Bi），代理人i不能通过某种推理从其初始信念导出一个信念p（Pi= Bp）.如果它们被限制到测试域P中的公式，它们就成为定义扩展基所需的约束。因此，这些规则的存在保证了从一个稳定模型得到的理论肯定是一个可拓基础（可靠性）。例4.2考虑例3.4中的理论P=（P1，P2，P3）P的测试域是LP=（{Pacifist}，{ Pacifist}），我们得到CP=（CP1，CP2，CP3）=（{}，{}，{Pacifist，<$Pacifist}）。从P转换的逻辑程序tr（P）如图2所示。 规则fact（3，Pacifist）← fact（3，Pacifist）.在（2）中描述了当主体3通过某种推理获得信念Pacifist时，他也可以通过命题逻辑推理获得信念现在我们给出一个定理，证明翻译前后的推理结果是相互对应的。定义4.3对于一组公式Pi和一个理论T =（T1，.， T n），我们大沼、小岛和永木65第一名（1，Pacifist）。(1)（2）第二次世界大战。事实（3，Pacifist）←bel（1，Pacifist），不是bel（3，<$Pacifist）。事实（3，<$Pacifist）← bel（2，<$Pacifist），不是bel（3，<$Pacifist）。事实（1，太平洋第一）。(2)fact (2,¬Pacifist).fact（3，<$Pacifist）← fact（3，<$Pacifist）.fact（3，Pacifist）←fact（3，Pacifist）.贝尔（1，太平洋第一）←不是贝尔（1，太平洋第一）。不是贝尔（1，太平洋第一）←不是贝尔（1，太平洋第一）。假的，假的，假的。假的，假的。贝尔（ 2 ， <$Pacifist ） ← 不 是 贝 尔 （ 2 ，<$Pacifist）。not bel（2，<$Pacifist）← not bel（2，<$Pacifist）.不假← bel（2，<$Pacifist），不是事实（2，<$Pacifist）。(3)不假，不假。贝尔（3，<$Pacifist）←不是贝尔（3，<$Pacifist）。不是贝尔（3，<$Pacifist）←不是贝尔（3，<$Pacifist）。假的←bel（3，<$Pacifist），不是事实（3，<$Pacifist）。不假←不是贝尔（3，<$Pacifist），事实（3，<$Pacifist）。3、不信，不信。不是贝尔（3，太平洋第一）←不是贝尔（3，太平洋第一）。假的← bel（3，Pacifist），不是事实（3，Pacifist）。假的，假的。图二、例4.2中的逻辑程序tr（P）定义一个算子reduceM如下：r导出M（Pi， T）={c|L1a1L1b1，1.. . L1b1，m（1）. ∧LnannLnbn，1.. . <$$>Lnbn，m（n）<$c∈Pi，aj∈Tj，bj，1， . ，bj，m（j）∈/Tj（j=1， . ，n）}。引理4.4设P=（P1，...，P n）是一个理论，S是一个稳定的模型，tr（P）. 则存在唯一的扩张基B =（B1，.，B n）的P大沼、小岛和永木66nn{|∈ }nn使得S={be l（i，p）|p∈Bi}i=1∪{not bel（i，p）|p∈（LPi− B i）}i=1fact（i，p）|p∈B i约化M（P i，B）}.i=1引理4.5设P=（P1，...，Pn）是一个理论，且B=（B1，...，B n）是P的扩张基。 然后S={be l（i，p）|p∈Bi}i=1∪{not bel（i，p）|p∈（LPi− B i）}i=1fact（i，p）|p∈B i约化M（P i，B）}i=1是tr（P）的稳定模型，即， S=Treduct（tr（P），S）↑ω.从这些引理，我们可以证明下一个结果。定理4.6设P是正规形理论，tr（P）是P的平移. 则P的扩张基与tr（P）的稳定模型之间存在一一对应。 扩展基B =（ B1，...， B n）和稳定模型S满足Bi=pbel（i，p）S（i = 1，...， n）。这个定理保证了对于任何可拓基都存在一个稳定的模型。因此，如果逻辑程序的所有稳定模型都从对MAEL的一个理论进行了计算，得到了该理论的所有扩张基。此外，我们可以从稳定模型中取出形式为bel（i，p）的原子并从中取出自变量，从而获得相应的扩展基。例4.7对于tr（P），存在两个稳定模型S和SJ步骤4.2：S={bel（1， Pacifist），bel（2，<$Pacifist），bel（3，<$Pacifist），not bel（3，<$Pacifist），事实（1， Pacifist），事实（2，<$Pacifist），事实（3， Pacifist），事实（3，<$Pacifist）}，nn大沼、小岛和永木67MMAAELTeoryMAEELLNNFTTTHEORYLLoogicPrograammP' 1P'PPP1P2ttrr（（P）P'Pnn不不1B1BT2B2S不1：1的比例B1：1的比例nnEExxtennsionsExtensionnBBasesssStablleMddeels图三. MAEL与逻辑程序SJ={bel（1， Pacifist），bel（2，<$Pacifist），bel（3，<$Pacifist），not bel（3，<$Pacifist），事实（1，Pacifist），事实（2，<$Pacifist），事实（3，<$Pacifist）}。对应于S的扩展基B是B =（{Pacifist}，{Pacifist}）。另一方面，对应于SJ的扩张基BJ是BJ=（{Pacifist}，{<$Pacifist}，{<$Pacifist}）。这一结果与实施例3.4一致。由于tr（P）的稳定模型除了S和Sj之外不存在，所以根据定理4.6，P的扩张基除了B和Bj之外此外，根据定理3.3，除了分别对应于B和BJ的T和Tj之外，不存在P本文中所示的所有对应关系如图1所示3.第三章。5讨论在本节中，我们讨论了MAEL中推理的性质，以及通过本文提出的翻译与以前研究的关系。5.1与Junker结果的关系Junker[10]提出了一种方法，将缺省逻辑和AEL的扩展的计算减少到TMS的计算。由于已知TMS的语义与逻辑程序的稳定模型语义一致[2]，因此Junker考虑到其特点，大沼、小岛和永木68˜˜TMS，即，由于有限性和逻辑推理能力的缺乏，Junker证明了缺省逻辑和AEL理论的扩展是以有限扩展基为特征的，并提出了一种可以计算扩展基的证明。事实上，MAEL中的可拓基和定义4.1中的程序规则（1）和（2）是通过将Junker的结果自然地扩展然而，Junker的用于AEL计算扩展的TMS并不符合逻辑程序的稳定模型语义，因为他改变了TMS的语义，使得可以允许公正的流通。另一方面，在不改变MAEL语义和稳定模型语义的情况下，逻辑程序，我们已经将这两个系统直接关联在本页中-per.这成为可能的原因是MAEL语义的弱可解释性[11]是用程序规则来描述的（见5.4节5.2扩张的有限理论根据定义2.5，MAEL理论的任何扩展都成为包含有限个公式的然而，如果一个理论是一组有限的公式，那么这个理论的一个扩展可以用它的有限子集来刻画。用定义3.2中定义的可拓基刻画可拓就是一种方法。虽然本文的翻译方法不要求MAEL理论的有限性，但如果理论是有限的，那么翻译后的逻辑程序将包含有限个程序规则。另一方面，稳定模型的计算系统[1，15]需要逻辑程序的有限性。因此，当我们考虑使用现有系统来计算翻译后的逻辑程序的稳定模型时，我们希望为一个扩展可以被有限地表征的理论生成一个有限的逻辑程序。本文的翻译方法表明，如果MAEL理论是有限的，则翻译后的逻辑程序是有限的5.3与绑架的Satoh[18]提出了一种方法，该方法将溯因框架中的解释计算他呼吁一个原子，可作为一个假设abducible，并给出以下规则对任何abduciblep：p←notp.p不是p。这个规则对将稳定模型分为p保持的模型和p保持的模型。在前者中，p作为一个假设成立，没有任何其他条件。大沼、小岛和永木69¬{}{}{}由定义4.1中的翻译规则（3）生成的前两个规则与此规则对的形式相同。实际上，给出规则的目的是建立一个模型，使bel（i，p）成立，即bel（i，p）是可溯的。本文中的翻译方法可以被认为是基于溯因的观点，因为在MAEL中形式化的推理如下：(i)假设Meta信念Li p或<$Li p被保持。(ii) 验证（i）中的假设是否满足理论的稳定性。转换规则（3）根据程序规则描述该视图，其中(i) 的描述使用的表示方法，Satoh提出的可展性，和（ii）描述使用完整性约束。5.4弱基语义如第5.3节所述，需要不仅将Li p而且将Li p视为假设的方法来描述MAEL语义的弱约束性[11]。粗略地说，弱序性意味着允许信仰的循环正义化。比如说， MAEL给出了两个扩展T=（L1p，. . ）和TI=（p，L1p，.. . ），理论P=（L1pp）. 因此，在弱可达性语义下，如果主体i可以通过假设Li p导出p，则他有一个信念p是有效的。为了考虑到这种语义，逻辑程序的模型中的推理在bel（i，p）被接受之后开始6结论为了发展MAEL的证明过程，本文证明了MAEL的可拓计算问题可以归结为逻辑程序的稳定模型计算问题为此，我们提出了一种从MAEL范式公式到具有完整性约束的程序规则的转换方法，并证明了保证推理结果不因转换而改变的定理。如果这种翻译有效，则可以将逻辑程序稳定模型计算的研究成果直接用于MAEL理论的可拓计算过程中。此外，为了阐明MAEL的推理性质，我们还通过翻译对MAEL的语义进行了表征。特别地，与[10]相比，我们形式化了能描述MAEL语义弱可拓性的逻辑程序.然而，正如在AEL[11]上所讨论的，弱推理性可能成为带来不期望的推 理 结 果 的 一 个 因 素 。 由 于 提 出 了 其 他 不 具 有 弱 连 续 性 的 se-mantics[11，14]，因此将它们应用于MAEL是解决该问题的候选者大沼、小岛和永木70引用[1] Cholew in'ski，P.， 诉W. Marek和M. 陈文辉，《企业信用风险管理系统》，第二版，第1996年，第518-528页。[2] 埃尔坎角，非单调真值维护系统的理性重构。内特尔43（1990），219-234.[3] 埃瑟林顿湾W.， 形式化非单调推理。内特尔31（1987），41-85.[4]Gelfond ， M. ， 和 V. Lifschitz ， 逻 辑 程 序 设 计 的 稳 定 模 型 语 义 学 ，Proc.5thICLP，（1988），1070-1080。[5] 汉克斯，S.，和D. McDermott，非单调逻辑和时间投影，Artiff。内特尔33（1987）379-412。[6] 本田，K.，K. Toyama和Y. Inagaki，基于解析的多智能体自认知逻辑决策过程，IEICE技术。报告，COMP 91 -97（1991）69-78。[7] 本田，K.，N. Kawaguchi，K. Toyama和Y. Inagaki，自动认知逻辑中基于归结的决策过程的效率改进，IEICE技术。Report，AI98-89，（1999）33-40.[8] 井上，K.，绑架原则，J.JSAI7（1992）48-59。[9] Iwayama，N.，和K.陈志荣，陈志荣，等.[10] 容克大学，和K.张文龙，“自认知逻辑与缺省逻辑的真值保持系统”，中国科学院学报，1990年，第8期，第278-283页。[11] Konolige，K.，论缺省与自认识逻辑的关系。内特尔35（1988）343-382。[12]Konolige，K.，Autoepistemic Logic，“ 人 工 智 能 和 逻 辑 编 程 中 的 逻辑 手 册 ” 3 （ 1 9 9 4 ） 2 1 7 - 2 9 5 。[13] 穆尔河，巴西-地C.的方法，非单调逻辑的语义学思考。内特尔25（1985）75-94。[14]尼梅拉岛赫尔辛基理工大学（1993年）。[15] 尼梅拉岛 和P. Simons，Sm odels-[16] 小川，H.，K. Toyama，K.，和Y.林志玲，多智能体自动认知逻辑的决策过程：公式转换方法，北京科技大学出版社. Report，AI95-62（1996）39-46.大沼、小岛和永木71[17] 赖特河，和G. Criscuolo，On Interacting Escherichia coli，Proc.7th IJCAI（1981）270-276。[18] Satoh，K.，和N.张文龙，利用磁共振技术计算外展，国立台湾大学机械工程研究所硕士论文（1991）。[19] Toyama，K.，Y. Inagaki和T.基于多自认知逻辑的持久性和因果性表示，J。 JSAI 12（1997）118-126.