理论计算机科学电子笔记123（2005）151-163www.elsevier.com/locate/entcs与Paralyes一起曼弗雷德·克尔伯计算机科学学院伯明翰大学伯明翰，B15 2 TT，英格兰电子邮件：M. cs.bham.ac.uk网址：http://www.cs.bham.ac.uk/~mmk/摘要一个好的知识表示系统必须在表达能力和一面是理性，另一面是理性。此外，有必要了解其局限性和问题。包含字符串的逻辑是非常有表现力的，并且允许非常自然的表示，这反过来又允许适当的推理模式。然而，这样一个系统的特点是它有可能在其中形成自我指涉悖论，这可以被认为是一个优点，同时也是一个弱点。 一方面，这是一个积极的一方面，它可以表示悖论，这可以在自然语言中制定。 另一方面，有必要谨慎，不要轻视逻辑系统。本文将讨论允许自指的知识表示的不同方面。将提出一个系统，这是一个务实的妥协之间的表达能力，一方面和简单性和效率的推理过程的另一方面。它建立在一个三值系统上，使得使用经典一阶逻辑的推理技术成为可能。保留字：字符串，悖论，三值逻辑1介绍逻辑悖论至少可以追溯到希腊先知埃皮门尼德（Epi- menides），他说：“所有希腊人都是骗子。”在一些额外的假设下，这导致了一个矛盾的情况。在最简洁的形式中，这个悖论可以用一句话来表述：“这个句子是假的。” 让我们假设它是真的，那么它一定是假的，因为它说它是假的。因此它必须是假的。这也导致了一个矛盾，因为如果它是假的，它的内容1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2004.04.046152M. Kerber/Electronic Notes in Theoretical Computer Science 123（2005）151悖论句的问题很早就被人们所知，但最初被认为与19世纪末/20世纪初的集合论和逻辑的发展无关。但是，集合论和逻辑中的悖论似乎危及了这一领域的进步，有一段时间，人们不清楚康托（希尔伯特称之为）建造的“集合的天堂”和弗雷格建造的策梅洛在[20]中提出了集合论的第一个公理化，罗素[16]在同一年提出了类型理论。这样（显然）就有可能把狮子关在外面。虽然在某种程度上，公理集合和类型的构造可以被认为足以用于数学推理，但在语言理解和更一般意义上的知识表示领域中有相当多的例子，在这些领域中，我们需要一种更强大的语言，在这些领域中，我们不能和/或不想仅仅基于语法理由而先验地如果我们这样做，我们最终会得到一个难以使用的系统。实际上，已经开发了相当多的复杂形式主义，并且目前正在AI的主流调查中，尽管一些更简单的系统可能会做得更好。Perlis在[14]中指出，我们“可以在一阶逻辑中拥有一切”。他研究了一个与我们在这里提出的系统很接近的系统，它我们的系统将在下一节中变得更加正式。在第3节中，我们明确了我们所说的悖论的第4节专门介绍三值Kleene逻辑，该系统将用于处理悖论。第5节描述了三值方法的有效推理形式。第6节介绍了一些相关工作。最后对全文进行了总结。2句法理论在我们介绍句法理论的形式句法之前，我们先介绍一些我们希望能够公式化的表达式然后我们固定一个语法，并讨论问题。现在让我们来看看一些典型的例子，这些例子是可以在句法理论中表示和推理的知识片段：(i) 约翰知道晨星就是昏星。K（John，“evening star = morning star”）(ii) 这句话是假的。L：真（(iii) 如果这是真的，那么。Lob：（True（模态逻辑与句法理论的关系对应于独立的、非独立的。M. Kerber/Electronic Notes in Theoretical Computer Science 123（2005）151153矩形与直接讲话戴维斯强调，直接言语更强大，因为特别是非句法表达可以直接表达，例如，（一个类似的属性适用于模态逻辑与句法逻辑，奥里。Konolige [11，p.114]提到了句法理论在知识表示的层次方法上的两个主要优势，首先是在这篇文章中，我们将更详细地看到处理悖论的三值方法;像说谎者句子这样的公式被承认，但它们既不是真的也不是假的，而是悖论。为了做到这一点，添加了第三个真值nn（代表“neither-nor”）。正如我们将看到的，仅仅添加这样一个真值并不能解决问题，而是系统必须满足一个额外的约束。然而，在我们进入语义分析之前，让我们要研究的语言是一种标准的一阶排序语言，加上字符串作为术语。除了标准设置之外，我们还在语言中使用字符串。为此，我们把字符看作语言中的常量符号。根据[3]中的描述，我们用冒号来前缀字符，例如，：C是字符C，：C是代表连接词的字符。此外，我们假设字符串上的二元函数符号pair，接受一个字符和一个字符串作为输入。 从空字符串ε中，我们构建 所有字符串，例如，pair（：C，pair（：a，pair（：t，ε）。由于这些表达式起着重要的作用，我们引入语法糖的表达式，如上面的符号可以定义和使用句法谓词符号。Variable（这种构造的细节可以在[5，第10章]中找到。排序代表一元谓词。也就是说，一个项t的排序是S（w ritten a sx和λx（x<$$> x）<$x也是无固定点的。如果我们将其中一个函数应用于三个真值false、nn或true中的任何一个，结果将永远不会与函数的输入相同。由此，悖论很容易被构建。然而，如果我们将语言限制在一个系统中，在这个系统中，每个可以从连接词构建的函数都至少有一个定点（方便的是，nn经常扮演这个角色），那么就不可能构建自指定点。这种限制似乎不是一个非常严重的，因为它很少希望沟通悖论。如果人们真的喜欢这样做，就必须去一个四值的设置（当然，它本身会有更高类型的悖论）。在一个三值设置中，没有一种语言包含连接词<$，和D，没有一种语言可以不受限制地使用<$和<$来保证定点的存在。但以nn为定点，λx x x有相同的定点nn也是（此外还有fixpointsfalse和true），并且fixpoint属性在复合下是守恒的。然而，这一限制不会阻止更微妙的建设，M. Kerber/Electronic Notes in Theoretical Computer Science 123（2005）151159¬∨{}≡∀≡►|悖论，其中我们通过定义一个二元函数f来构造悖论（仅使用<$和<$）在真值中，使得x：=f（x，y）对于固定的真值y 这将导致一个问题，如果xf（x，y）为所有可能的真理值x.在这种情况下，y 所以我们假设y=nn。是否有可能定义一个函数f，使得f（x，y）/=x对于x=true，x=nn，and x=false？这不是事实，因为当限制为false和true时，f也有范围{false，true}。为了在false，true上不受定点限制，f（x，y）必须是x，因为这是所有可能的16个这样的函数中唯一没有定点的函数。故其为真，故其为假，故其为真，故其为假。（通常有更多的fixpoints而不仅仅是nn。定理4.4任何由连接词和构造的函数都包含一个定点。定点性质的推论是定义形成保守扩张。现在让我们来看看为什么泛量化公式如A×B有一个定点。 如果x是一个字符串，它允许使用包含A的表达式进行实例化。如果B可以对于x的一个实例化为假，A为假。如果B对所有实例化都为真，那么A为真。在其他情况下（不可能实例化x得到一个假值，但它并不总是真的），我们可以选择nn作为fixpoint。给出这种可能性是因为连接词的命题系统不是完成.为了能够引入定义（就像说谎者句子的定义一样，但当然也包括更有用的句子），不能完全放弃连接词，而必须在定义中允许使用连接词，也就是说，以A.的形式。或 xA（x） .. . ，其中A是谓词常量。 这不会引起问题，因为如果A出现在右侧，右侧将有一个定点A，因此等价性总是可以为真。5因果关系与推理当我们放弃D连接词时，我们失去了语言中的大多数重言式，并且出现了这样的问题，当其中没有适当的重言式时，我们如何恢复非平凡系统。这可以通过考虑序列来实现，即，由一组公式Φ和公式A（写为Φ）组成的对A），其中Φ中的所有公式都假定为真。 语义等价物是模型关系Φ=A，其代表：在Φ的所有模型中，即，所有如果一个解释将Φ中的每个公式都求值为真，那么A也成立，也就是说，A也被求值为真。 一种建立在反驳基础160M. Kerber/Electronic Notes in Theoretical Computer Science 123（2005）151≡≡≡这个原理利用了Φ中的所有公式必须为真的事实，并驳斥了A可能为假或nn的假设。注意这种方法中Φ和A之间的不对称性，Φ中的公式由于我们使用的是一种没有D连接词的限制语言，因此可以使用[9]中描述的重用二值定理证明方法的策略来处理Kleene逻辑这意味着，有效标准通过增加一个简单的限制策略，二值定理证明器可以成为上述这就形成了一般一阶Kleene逻辑的演算。为了处理引用的表达式，我们必须添加公理模式来描述在其上定义的元谓词的语义。在真值谓词True的情况下，我们已经更仔细地研究过了，这意味着我们添加了来自备注4.3的规则，或相应的公理模式。[9]的主要结果是，可以使用包含nn的真值集和不包含nn的真值集的tableau规则之间的结构相似性。可以在这些规则中只删除nn。因为它通过使用组合规则（对于false，nn和nn，true）可以完全避免真值nn的规则，可以建立以下策略结果，这也允许使用标准的一阶定理证明技术用于Kleene逻辑。定理5.1（策略）设S是不封闭两个公式的tableau的控制策略，则使用S找到的每个二值tableau证明都可以提升为定理的三值tableau证明。注5.2[9]的结果留给我们的问题是如何处理有效连接。我们可以使用tableau规则来计算。然而，我们使连接词的使用仅限于定义因此，只有三个画面规则中的第一个（（A B）真）才是相关的。但是，即使是这个规则也会将场景分成三个场景，因此它是相当不合理的。更严重的是，上述战略结果不能保持。而不是使用这个规则，我们简单地假设在证明中所有的定义都可以扩展，也就是说，我们将定义扩展规则带入微积分中（对于任意的真值集合α）。Aα（AB）trueBα这个规则（以及处理True（因此，相应的定理也适用于我们的情况。M. Kerber/Electronic Notes in Theoretical Computer Science 123（2005）1511616相关工作关于悖论、悖论存在的原因以及如何处理悖论的方法，有大量的文献。这将是很容易填补书籍只是一个概述，这将是不可能给一个公平的帐户在这里。处理悖论的第一个解决办法可以追溯到罗素，这是很容易的，也是很聪明的，即简单地排除它们。罗素引入了类型，使得在形式P（Q）的任何表达式中，P必须具有比Q更高的类型。特别是P这种方法已经被塔斯基[17]改编为分层元系统，在其中可以明确地谈论陈述的真实性，但不是在语言本身中，而是在一些元语言中。如果一个人想对元语言做陈述，这也是可能的，但是他需要一个元-元语言。这种方法已经在多层次元系统FOL和Get- fol中得到了形式化和实现[6]。虽然这种方法适用于数学，但像水门悖论这样的例子表明，完全排除自指性（至少）在某些应用中是不合适的。完全禁止自我参照的另一种选择是限制它，把它放在正确的语境中。Barwise和Etchemendy在[1]中详细讨论了这种方法作为第二种方法，他们称之为Austinian方法。这个想法是以适当的方式限制自我指涉表达。应用到罗素的理发师的例子，这意味着，理发师的定义是“刮胡子的人，只有那些不刮胡子的人”是有问题的。但是，例如，将理发师定义为“只为所有住在牛津的人刮胡子的人，而不是自己刮胡子的人”，这只意味着理发师不住在牛津。虽然我同意，许多乍一看似乎自相矛盾的情况可以澄清，从而消除悖论，但某些句子是故意自相矛盾的。Kripke [12]和其他人通过改变公式真值的语义结构来解决这个问题它们超越了二值逻辑，它们假设了第三个真值，这代表了悖论表达式。有不同的方法，要么假设真值间隙[4]，要么假设第三个真值，它明确地声明了欠确定性[10，p.332-340]。在这两种体系中，塔斯基is，True（也 在第一个具有真值间隙的系统中，没有真值被分配给说谎者句子L。在第二种情况下，L被评估为真值nn，特别是True（问题是如何确定这些表达式中的真值。为此，Kripke提出了一个定点迭代器，一个过程，在每次迭代中，真值被分配给更多的，162M. Kerber/Electronic Notes in Theoretical Computer Science 123（2005）151更多公式Kripke这样一种一般性的办法对于一般性的办法是必要的它已经变得更加正式，特别是Barwise和Etchemendy [1]给出了语义解释。他们使用Aczel的超集理论（不满足基础公理的集合）来模拟自指性。在[2]中给出了更详细的描述。McGee也提出了类似的方法[13]。在Perlis改变为L和<$True（“L“）同时成立的系统本文提出的方法可以被看作是一个限制版本的Barwise和Etchemendy所谓的罗素方法。它建立在作者早期的工作[7]上，并且与Ramsay的方法[ 15 ]密切相关7总结在这篇文章中，我们看到了一种三值方法，它允许在一个形式系统中几乎没有任何限制地使用自指句。我们必须对这样一个系统施加的唯一限制，是保证任何定义都能给我们一个定点。对于表语定义，这可以通过只使用标准连接词而排除允许谈论悖论的连接词的定义来保证。第一种观点认为，这似乎使系统变得平凡，因为通过这种限制，我们已经从系统中消除了几乎所有的重言式。然而，当我们假设一个背景理论时，关于推理发生，这根本不是一个严重的限制。背景理论中的所有公式都被假设为真（这相当于说，它们不是假的，也不是悖论的）。如果我们假设背景理论中的一个悖论公式为真，那么系统就变得不一致（而不是悖论），就像经典系统通过假设一个公式及其否定而变得不一致有趣的是，对连接词的限制允许将标准的二值定理证明技术转移到三值情况。总而言之，我们已经提出了一个关于真理的陈述事实的系统。通过添加更多的公理模式，有可能扩展框架来处理知识和信念。为了避免自我指涉的陈述，对表达能力没有任何不自然的限制如第5节所示，可以使用标准结石。 在这项工作中，我们没有产生 True谓词的正式定点构造，但仅给出了为什么存在此类定点的指示。在Kripke、Barwise、Etchemendy和Moss的工作基础上，这应该是可能的，但作为未来的工作。M. Kerber/Electronic Notes in Theoretical Computer Science 123（2005）151163引用[1] Jon Barwise和John Etchemendy。《说谎者：论真理与循环》（The Liar牛津大学出版社，纽约，美国，1987年。[2] 乔恩·巴怀斯和劳伦斯·莫斯恶性循环CSLI Publications，Stanford，California，USA，1996.[3] 欧内斯特·戴维斯。常识的代表。摩根考夫曼，圣马特奥，加利福尼亚州，美国，1990年。[4] 巴斯角 范·弗拉森。奇异项、真值缺口和自由逻辑。哲学杂志，LXIII（17）：481[5] Michael R. Genesereth和Nils J. Nilsson。人工智能的逻辑基础。摩根·考夫曼，美国加利福尼亚州圣马特奥，1987年。[6] 福斯托·金奇格里亚Getfol手册IRST-技术报告9107-01，IRST，特伦托，意大利，1994年。[7] 我是K er ber。 关于知识、技能和技能。 在J. 迪克斯湖FarinasdelCerro，and联合Furbach，编辑，JELIA '98会议记录施普林格出版社，柏林，1998年。LNAI 1489[8] Manfred Kerber和Michael Kohlhase。部分函数的表演算。CollegiumLogicumm-AnnalsoftheKurt-Godel-Socityity，2：21-49，1996.[9] Manfred Kerber和Michael Kohlhase。不需要重新实施就能实现机械化在G.布鲁卡角Habel，和B. Nebel编辑，《KI'97会议记录》施普林格出版社，柏林，LNAI1303。[10] 斯蒂芬·科尔·克林。元数学导论。范诺斯特兰德，阿姆斯特丹，荷兰，1952年。[11] 科特·科诺利格。 一个信念的演绎模型。 皮特曼，伦敦，1986年。[12] 索尔·克里普克真理理论概要哲学杂志，LXXII：690[13] 范·麦基真理、模糊与悖论哈克特出版公司，印第安纳波利斯，美国，1990。[14] 唐纳德·佩里斯。自指语言I：基础（或：我们可以在一阶逻辑中拥有一切！）AI，25：301[15] 艾伦·M拉姆齐无类型构造性λ-演算的定理证明：实现和应用。Logic Journal of theIGPL，9（1）：83[16] 伯特兰·罗素。以类型理论为基础的数理逻辑。American Journal of Mathematics，XXX：222[17] 阿尔弗雷德·塔斯基Wahrheitsbegri在正式的语言中是不可缺少的。Studia philosophia，1：261[18] 阿 拉斯 代 尔 · 厄 克特多 值逻 辑In D.Gabbay 和 F.Guenthner ， editors ， Handbook ofPhilosophical Logic，chapter III.2，pages 71-116. Reidel，Dordrecht，荷兰，1986年。第三卷：经典逻辑的替代品。[19] 克里斯托夫·魏登巴赫第一阶舞台布景与排序。Journal of the Interest Group in Pure andApplied Logics，IGPL，3（6）：887[20] 他 叫 泽 梅 洛 。UntersuchunggenuüberdiieGrundlagenderMengenlhre 。 I.MatheMatischeAnnalen，65：261 -2 8 1 ， 1 9 0 8 .
我的内容管理
展开
