论文部分内容阅读
人工智能领域中的一个极具有挑战性的研究方面是自动推理(定理机器证明),归结自动推理是自动推理的重要研究方向之一,其研究成果已被应用到很多重要领域,如人工智能、逻辑编程、问题求解、软件模型检测与测试、安全协议、程序自动验证、应答系统等方面。现实世界中经常遇到一些由于其多因素而产生不可比较性的问题,这类带有不可比较性信息的问题往往很复杂。基于格蕴涵代数的格值逻辑系统的归结自动推理是解决这类问题的有效方法之一。本文在其他学者的工作基础上,依据经典逻辑的归结推理方法,对基于格蕴涵代数的格值逻辑系统的α-多元线性归结自动推理的理论、方法、算法、程序展开研究。取得的研究成果主要有以下五个方面:第一部分,在基于Lukαsiewicz蕴涵代数Ln的格值命题逻辑系统LnP(X)中,得到了一类3阶不可分极简式(3-IESF)所有可能的形式,针对其中一类特别重要的3-IESF,给出了它与n-IESF(0≤n≤3)之间的α -可归结性。第二部分,在基于格值逻辑系统的α-多元归结原理的基础上,针对广义文字所有分类的分界广义文字,给出了它们之间任意三个广义文字的α-可归结性,进一步得到了格值逻辑系统中的α-多元归结域的一些性质。第三部分,进一步在基于格值命题逻辑系统LP(X)的α-多元归结原理基础之上,提出了基于格值命题逻辑系统LP(X)的α-多元极小归结原理,建立了 LP(X)中的α-多元极小归结原理的可靠性和完备性。然后,基于LP(X)的α-多元极小归结原理,建立了基于LP(X)的α-多元有序线性极小归结方法,并建立了基于LP(X)的α-多元有序线性极小归结方法的可靠性和条件完备性定理,分析了基于LP(X)的α-多元有序线性极小归结方法的有效性。进一步,构造了基于LP(X)的α-多元有序线性极小归结自动推理算法,为了提升该算法的归结效率,给出了广义子句集预处理的方法和选取广义文字及判定时的六个策略,然后证明了 α-多元有序线性极小归结自动推理算法的可靠性和完备性,对该自动推理算法的时间复杂度进行了分析,给出了一个例子进行阐述算法的有效性,设计了基于LP(X)的α-多元有序线性极小归结自动推理程序。第四部分,提出了基于格值一阶逻辑系统LF(X)的α-多元极小归结原理,得到相应的提升引理,并证明了基于LF(X)的α-多元极小归结原理是可靠和完备的,进而得到了α-多元极小归结原理的等价转换定理。然后,基于LF(X)的α-多元极小归结原理,建立了基于LF(X)的α-多元有序线性极小归结方法,并建立了基于LF(X)的α-多元有序线性极小归结方法的可靠性和条件完备性定理,得到了 α-多元有序线性极小归结方法的等价转换定理,分析了基于LF(X)的α-多元有序线性极小归结方法的有效性。进一步,构造了基于LF(X)的α-多元有序线性极小归结自动推理算法,证明了该算法是可靠且完备的,并给出了一个例子进行阐述α-多元有序线性极小归结算法的有效性。第五部分,为了进一步提高α-归结能力和归结效率,针对广义文字归结的α-多元极小归结进一步提升,提出了基于格值命题逻辑系统LP(X)的非子句α-多元极小广义归结原理,并证明了该广义归结原理是可靠和完备的。提出了基于LP(X)的非子句α-多元有序线性广义归结方法,得到其可靠性和条件完备性。然后,基于非子句α-多元有序线性广义归结方法,构造了 LP(X)中的一个非子句α-多元有序线性广义归结算法。进一步,将基于格值命题逻辑系统LP(X)的非子句α-多元极小广义归结原理推广到LF(X)中,提出了基于格值一阶逻辑系统LF(X)的非子句α -多元极小广义归结原理,给出了相应的提升引理和等价转换定理,证明了该广义归结原理是可靠和完备的。接下来,提出了基于LF(X)的非子句α-多元有序线性广义归结方法,得到了其可靠性和条件完备性。最后,基于非子句α-多元有序线性广义归结方法,构造了 LF(X)中的一个非子句α -多元有序线性广义归结算法。