基于格值命题逻辑系统LP(X)的多元α-归结原理的注记

进一步深入研究了基于格蕴涵代数的格值命题逻辑系统LP(X)的多元α-归结原理的基本理论,给出了基于LP(X)的多元α-归结演绎中参与多元α-归结的广义文字个数随着归结演绎的推进而动态变化的基本原则;对基于LP(X)的多元α-归结原理的有效性进行了一定分析,这为建立基于LP(X)的多元α-归结方法以及构造多元α-归结算法奠定了理论基础.     

命题逻辑中非子句α-有序线性广义归结方法

为了处理在不确定性环境下的自动演绎,重点研究了基于自动推理理论的归结方法,其自动推理理论是真值定义在格蕴涵代数（lattice implication algebra,LIA）结构上格值逻辑系统中的。在已有的确定真值水平α二元归结研究的基础上,作为其继续研究和扩展,引入了基于格值命题逻辑系统LP( X )的非子句多元α-有序线性广义归结方法和演绎,这从本质上避免了一个非子句广义归结演绎到规范子句的形式。随后,得到LP( X )中的非子句多元α-有序线性广义归结演绎是可靠和完备的。该研究工作为格值命题逻辑中基于自动推理的归结提供了一个更有效的方法。     

语言真值格值命题逻辑中的α-语义归结方法

语言值智能信息处理是人工智能的一个重要研究方向,基于归结原理的自动推理因易于在计算机上实现而得到广泛研究。为了提高基于语言真值格值逻辑的α-归结原理的效率,将语义归结策略应用于α-归结原理,研究了基于格值逻辑的归结自动推理方法。首先给出了语言真值格值命题逻辑系统的α-语义归结与L_nP(X)中相应归结水平的语义归结之间的等价性,并通过实例说明其有效性。接着,给出了语言真值格值命题逻辑系统的α-语义归结算法,并证明了该算法的可靠性和完备性。     

格值一阶逻辑LF(X)中的α-语义归结方法

自动推理是人工智能的一个重要研究方向,基于归结原理的自动推理因易于在计算机上实现而得到广泛研究。语义归结是对归结原理的一种改进,它利用限制参与归结子句类型和归结文字顺序的方法来提高推理效率。为了提高基于格蕴涵代数的格值逻辑的α-归结原理的效率,将语义归结策略应用于α-归结原理。首先给出了格值一阶逻辑系统中的α-语义归结概念和α-语义归结演绎概念,接着讨论了格值一阶逻辑系统的α-语义归结方法,并证明了其可靠性和条件完备性,最后通过实例说明了其有效性。     

直觉模糊逻辑的(α,β)-准锁语义归结方法*

为了提高直觉模糊命题逻辑的(α,β)-归结效率,将准锁语义归结策略应用于(α,β)-归结原理,得到直觉模糊命题逻辑的(α,β)-准锁语义归结方法,证明方法的可靠性与完备性.给出直觉模糊命题逻辑系统的(α,β)-准锁语义归结和(α,β)-准锁语义归结演绎的概念.讨论直觉模糊命题逻辑系统中的(α,β)-准锁语义归结式和锁子句的合并规则.最后,给出直觉模糊命题逻辑系统的基于(α,β)-准锁语义归结的自动推理算法步骤,并通过实例说明算法的有效性.     

格值命题逻辑系统中广义文字的正规性

基于格蕴涵代数的格值命题逻辑系统能定性地刻画不可比较性和不精确性。广义文字是该系统中α-归结自动推理的核心概念,是α-归结中的最基本单元。公式的正规性是α-归结原理中保持完备性的重要条件,其语义性质是公式形式的重要反映。从语义角度研究了广义文字的正规性,给出了两种典型正规公式F1→F2和(F1→F2)'的真值情况。为讨论广义文字的形式及其α-可归结性提供了理论基础。     

具有三种否定的模糊命题逻辑形式系统FLCOM的λ-归结

考虑到模糊逻辑中定理自动证明的重要性以及目前主要研究具有一种否定的模糊逻辑的归结原理,文中对具有三种否定(矛盾否定、对立否定和中介否定)的模糊命题逻辑(FLCOM)的归结原理进行研究.基于FLCOM的一种无穷值语义解释提出λ-可满足的和λ-不可满足的概念.将λ-归结方法引入FLCOM,给出FLCOM的λ-归结演绎定义,讨论FLCOM的λ-归结原理,并证明FLCOM的λ-归结方法的完备性.基于λ-归结方法和已证明的结论给出实例以佐证文中λ-归结方法和结论的正确性和可行性.因此,在FLCOM范围内可判定任一模糊命题公式是否是λ-可满足的或λ-不可满足的.     

直觉模糊逻辑的（α,β）-广义锁归结方法

归结方法是定理自动证明的重要工具。为了简化直觉模糊命题逻辑的归结过程,基于直觉模糊命题逻辑归结原理的一般形式,提出了子句(αβ)-可满足和(αβ)-归结式的概念。研究了广义子句与其归结式的可满足性。在直觉模糊命题逻辑系统中给广义子句配锁,规定在做归结时各子句中被消去文字在该子句中的序号最小,由此建立了(αβ)-广义锁归结方法,并证明了该方法的可靠性和完备性。给出了直觉模糊逻辑的广义锁归结算法步骤,并通过实例说明了该方法的有效性。     

多元动态演绎在Prover9证明器中的应用

Prover9证明器只采用二元归结方法,是一种静态的、局部的推理规则。基于矛盾体分离规则,提出了一种多元动态演绎算法,采用整体式演绎框架,通过子句演绎权重与文字演绎权重规划演绎路径,并带有回溯机制搜索较优路径。以CADE2017竞赛例(FOF组)进行测试,加入多元动态演绎算法的Prover9证明器证明定理总数提高了40.7%,且所用的平均时间降低了7.46 s。实验表明,提出的多元动态演绎算法是一种有效的推理方法,能有效提高一阶逻辑自动定理证明器的能力。     

命题逻辑中一种矛盾体生成新方法

人工智能是用计算机来模拟人的某些思维过程和智能行为的学科。自动推理中的归结原理是一种简洁、可靠且完备的推理规则。矛盾体的动态多子句协同演绎理论不仅是归结原理的重要延拓，而且具有较高的推理演绎效率。由于矛盾体的结构复杂、生成策略较少，因此在矛盾体的动态演绎可靠性和完备性的基础上，提出复合2个或多个矛盾体的部分子句的不同策略，为矛盾体的构造提供了一种有效的方法。     

归结原理及其应用

归结演绎推理是一种在计算机上得到较好实现的基于归结原理的推理技术,介绍归结原理的基本思想以及它在自动推理中的应用。     

粒计算研究现状及基于Rough逻辑语义的粒计算研究

综述了粒计算的提出背景、研究现状及其发展趋势,也给出了作者的评论;论述了粒计算应用的广泛性,包括AI中的图像检索、医学诊疗系统、连续数学中的积分学及其它许多逻辑推理等方面的应用.讨论了粒计算将有希望成为处理信息和研究其它学科的理论工具和方法学.讨论了粒计算中基于Rough逻辑语义的粒及其相关性质,建立了这种粒的演绎推理.提出了基于Rough逻辑语义的粒归结原理和归结策略,包括λ-归结策略和锁归结策略.证明了这种粒归结的完全性.基于Rough逻辑语义的粒在AI的问题求解、专家系统以及机器定理证明中都将成为一种新的研究思想和新的理论工具.最后,提出了这种基于Rough逻辑语义的粒计算研究前景.     

基于格值一阶逻辑LF（X）的自动推理算法

基于谓词逻辑的归结推理方法是目前理论上较为成熟、可以在计算机上实现的推理方法之一。针对格值一阶逻辑LF(X)中归结自动推理问题,以格值一阶逻辑LF(X)的α-归结原理为理论基础,通过对例子进行分析,提出了LF(X)中简单广义子句集的归结自动推理算法,并证明了该算法的可靠性和完备性。     

命题逻辑中一类正则标准矛盾体的构造与复合

归结原理是自动推理中一种简洁、可靠且完备的推理规则，标准矛盾体分离演绎理论是二元归结的一个延拓。矛盾体的结构非常复杂，现有的矛盾体种类和生成策略较少。针对该问题，文中基于命题逻辑的标准矛盾体分离演绎理论，首先通过复合两个或多个正则标准矛盾体，得到了生成新矛盾体的多个复合策略；其次，提出了一类特殊标准矛盾体结构——复合正则标准矛盾体，丰富了矛盾体的结构特征；然后讨论了复合得到的新矛盾体不同子句的可扩充性，进而得到相应的文字添加策略；最后，提出了矛盾体的生成算法，为进一步在计算机上实现新矛盾体的生成提供了参考。     

使用XML的一阶谓词逻辑归结原理

归结原理(resolution principle)是计算机自动推理的重要原理之一.将XML加入到使用归结原理的证明过程中,利用XML结构与语义自描述的特性,简化归结过程的计算机实现,并给出相应基于XML的算法.     

具备归纳和演绎能力的数据库系统Duce—92的设计与实现

一、引言演绎数据库是近几年数据库研究的热点。根据 Grant 和 Minker 的分类,演绎数据库的研究可以分为三个阶段:第一阶段(1957—1968),开始了演绎数据库的研究工作,开始应用 J.A.Robinson 提出的归结原理于演绎数据库中的演绎的实现。第二阶段(1969—1978),逻辑程序设计和 Prolog 在演绎数据库中的应用;演绎数据库语义和否定在定义数据库中的研究。第三阶段(1979     

模糊集间的R_0-相似关系及其性质

将王国俊教授在R0-型逻辑系统中建立的R0-蕴涵算子应用于模糊数学理论之中,在非空集合X为论域的模糊集族F(X)上定义了一种新型运算-R0蕴含运算,并讨论了F(X)上R0-蕴含运算的一些基本性质。通过R0-蕴含运算在F(X)上定义了一个二元模糊相似关系-R0-相似关系,并对其性质进行了较为详细的讨论。在有限论域X确定的模糊集族F(X)上给出了几个R0-相似关系的具体实例。     

RLD演绎及子句蕴含与子句包含关系的非等价性

软件复用的一个主要任务是可复用软件构件的表示与检索，由于一阶逻辑能够描述软件构件的计算语义，因此用一阶逻辑表示构件及用基于归结原理的自动定量证明技术检索构件的研究在软件工程领域得到了足够的重视，为了简化基于演绎的构件检索技术的程序设计结构及提高演绎效率，提出了最右线性演绎RLD（rightmost linear deduction)，并证明了它的完备性，同时，指出了子句蕴含与子句包含关系的非等价性，并给出了由子句蕴含关系推出子句包含关系成立的一个充分条件。     

使用XML的一阶谓词逻辑归结原理

归结原理（resolution principle)是计算机自动推理的重要原理之一。将XML加入到使用归结原理的证明过程中，利用XML结构与语义自描述的特性，简化归结过程的计算机实现，并给出相应基于XML的算法。     

命题模态归结的一种变型

本文给出了模态子句集的标准子句集概念，提出了一种基于标准子句集的模态归结方法的变型，称之为标准模态归结，证明了任意模态子句集恒假当且仅当存在从它的标准子句集出发，使用标准模态归结推出空子句的演绎，从而证明了对于不可满足标准子句集、标准模态归结是完备的，这种标准模态归结，揄规则简单、直观且容易实现。