认识逻辑(3):基于语义tableau的证明理论

本文定义了带有索引的认识逻辑ELI,讨论了ELI的语义tableau的证明过程,证明了模态tableau的相容性和完备性.由于ELI与认识逻辑EL是等价的,因而,本文讨论的tableau证明过程也可以作为EL的证明理论.     

基于语义tableau的一阶逻辑自动定理证明

自动推理作为自动定理证明的扩展是人工智能研究的基础工作,许多重要的人工智能系统都是以推理系统为其核心部分,其中的tableau方法,由于具有通用性、直观性及易于计算机实现等特点,至今成为重要的自动推理方法之一。在tableau方法基础上,讨论了一阶逻辑中的自动定理证明理论,提出使用模型存在定理证明其可靠性和完备性的方法。同时也给出了带等词tableau方法的证明过程。     

基于tableau结点封闭值的非一致性数据库开放分支修复方法

在将tableau方法扩展到非一致性数据库修复的基础上,提出一种新的利用分支封闭值修复数据库的方法。该方法结合tableau分析法的开放和封闭推理标准,以开放公式树TP(IC∪r)分支为基础,为公式树TP(IC∪r)中每个结点引入一个结点封闭值。根据TP(IC∪r)中结点封闭值的定义,通过计算TP(IC∪r)的结点封闭值来选择分支进行开放修复,从而可以直接确定数据库的修复实例,同时考虑了含有I封闭的修复,将开放修复扩展到含有I封闭的TP(IC∪r),并给予逻辑证明。最后,对于一致性应答结果的逻辑特征予以证明。     

自由变量语义tableau中δ-规则的一种改进方法

自动推理一直是人工智能领域研究的重要内容．近几年来，由于tableau方法的通用性和直观性，引起人工智能界的广泛关注．对于自由变量语义tableau中的量词规则，由于r-规则替换的任意性，可导致在同一tableau证明中r-规则被多次使用，使得tableau推理结构树中出现多个自由变量．针对tableau中多次出现自由变量，使tableau封闭延迟的问题，在δ^ -规则的基础上，提出对δ^ -规则改进的δ^ -规则，并进行了正确性证明．将δ^ -规则应用到TableauTAP系统中，结果表明，δ^ -规则使tableau封闭提前，在推理的时间效率和空间效率上都有较大的提高．     

一种逻辑强化学习的tableau推理方法

tableau方法是一种具有较强的通用性和适用性的推理方法，但由于函数符号、等词等的限制，使得自动推理具有不确定性，针对tableau推理中封闭集合构造过程具有盲目性的问题，提出将强化学习用于tableau自动推理的方法，该方法将tableau推理过程中的逻辑公式与强化学习相结合，产生抽象的状态和活动，这样一方面可以通过学习方法控制自动推理的推理顺序，形成合理的封闭分枝，减少推理的盲目性；另一方面复杂的推理可以利用简单的推理结果，提高推理的效率。     

利用tableau方法修正Deep Web中不相容知识

在分析Deep Web中不相容知识的单调性、动态性、模糊性的基础上,提出了基于tableau的不完备知识处理的模型生成方法IK-tableau。该模型采用非经典逻辑表示方法,将Deep Web信息表示为逻辑公式集合,采用模型生成算子对逻辑公式进行扩展。通过IK-tableau方法,能够找出Deep Web搜索中的不完备知识,并可以进行修正,生成知识模型;同时利用该模型可以进一步指导Deep Web搜索。     

翻译成整数规划的IP-tableau方法

由经典命题公式对应着0-1-整数规划的事实,提出将tableau方法与整数规划相结合的IP-tableau方法,并提升到一阶逻辑、多值逻辑以及无穷值逻辑。将tableau转化为IP方法后,可以采用许多提高IP效率的方法。另外在多值逻辑中,随着n值的增加,IP问题不会变得更加复杂。     

一种多值规则量词公式的tableau的方法

在多值逻辑中，含有量词的tableau方法具有统一的扩展规则，并已通过可靠性和完备性的证明。但是由于扩展后的分枝非常庞大，使机器实现非常困难。文章通过对规则量词公式与一阶经典量词公式的对应关系的研究，使二者使用统一的扩展规则。     

一种含等词的分阶段Tableau算法

在增强新的扩展规则的tableau方法的基础上提出了一种新的含等词tableau算法—分阶段tableau。在该算法中，将tableau四分成两个阶段，等词单独处理，利用提取不等式析取并在启发式的帮助下计算等价类的方法，进一步限制了tableau的搜索空间，提高了tableau的推理效率。同时，为了研究分阶段tableau的有效性，进行了实例分析，并与Fitting和Jeffrey方法进行了比较，结果表明，分阶段tableau方法优于其它方法。     

中介命题演算系统MP^M的公理完备集

本文基于中介逻辑命题演算系统MP^M构造了一个公理集合，证明了该公理集合的完备性。该公理集合中的公理均是由等式的形式给出，可以方便地对MP^M、MF^M系统上的等值公式进行推导和证明。本文还讨论了该公理集合在不完全信息数据库查询优化上的应用。     

Tableau Methods for a Logic with Term Declarations

We study free variable tableau methods for logics with term declarations. We show how to define a substitutivity rule preserving the soundness of the tableaux and we prove that some other attempts lead to unsound systems. Based on this rule, we define a sound and complete free variable tableau system and we show how to restrict its application to close branches by defining a sorted unification calculus.     

一种基于符号变换的描述逻辑ALC超协调推理算法

语义万维网作为一个开放、不断更新而且相互协作的环境,经常会包含一些不协调的或不精确的信息。众所周知,描述逻辑是语义万维网重要的逻辑基础,然而描述逻辑缺乏处理不协调或不完全信息的能力。近来一些超协调方案通过限制或阻止使用一些推理规则来避免推理的平凡化,从而容忍本体中出现的不协调。因为这些方法限制了描述逻辑系统的推理能力,所以推理能力弱于经典的描述逻辑推理能力,即使在处理协调的本体时。提出一种基于符号变换的具有强推理能力的超协调推理算法。证明了该算法是可判定的,而且在处理协调的本体时该推理系统与经典逻辑系统具有相等的推理能力。     

一种求解tableau等式合一问题的算法

在增添扩展规则的tableau方法的基础上提出了一种新的含等词tableau方法——等式合一方法，并证明了它的可靠性和完备性。在该方法中，将tableau分成两个阶段，等词单独处理，通过提取等式合一问题并求解解替换封闭tableau，进一步限制了tableau的搜索空间，提高了tableau的推理效率。同时，为了研究等式合一方法的有效性，在解替换求解方面，提出了提取不等式析取，并在启发式的帮助下计算等价类的方法。通过实例分析，结果表明，等式合一方法优于其它方法。     

从ALC到SHOQ（D）：描述逻辑及其Tableau算法

描述逻辑是一类知识表示的形式系统，并成为语义Web的逻辑基础。Tableau是描述逻辑的基本证明论，基于Tableau的算法提供7描述逻辑的推理机。本文系统地阐述了对应于语义Web语言从基本的ALC到SHOQ(D)描述逻辑基础及其相应的Tableau算法。     

First-order modal tableaux

We describe simple semantic tableau based theorem provers for four standard modal logics, in both propositional and first-order versions. These theorem provers are easy to implement in Prolog, have a behavior that is straightforward to understand, and provide natural places for the incorporation of heuristics.     

Cut and Pay

In this paper we study families of resource aware logics that explore resource restriction on rules; in particular, we study the use of controlled cut-rule and introduce three families of parameterised logics that arise from different ways of controlling the use of cut. We start with a formulation of classical logic in which cut is non-eliminable and then impose restrictions on the use of cut. Three Cut-and-Pay families of logics are presented, and it is shown that each family provides an approximation process for full propositional classical logic when the control over the use of cut is progressively weakened. A sound and complete semantics is given for each component of each of the three families of approximated logics. One of these families is shown to possess the uniform substitution property, a new result for approximated reasoning. A tableau based decision procedure is presented for each element of the approximation families and the complexity of each decision procedure is studied. We show that there are families in which every component logic can be decided polynomially.Partly supported by CNPq grant PQ 300597/95-5 and FAPESP project 03/00312-0.     

基于概念的折半查找算法

自顶向下或自底向上两种标准查找方式不适合于具体领域逻辑,且缺乏灵活性.模拟有序数组中的折半查找,提出逻辑空间上的折半查找方法,证明该查找方法在保持完备性和非冗余性的同时,还提供了更好的灵活性,最后给出了该查找的通用算法,并分析其复杂性.