论文部分内容阅读
自动推理(定理机器证明)是人工智能领域基本课题之一,而归结自动推理是“自动推理(定理机器证明)”的一种有效方法,其研究成果可以广泛应用于各种人工智能系统,如自然语言理解、问题求解、程序自动设计和程序自动验证等方面。现实中,存在-类非常典型的不确定性,即不可比较性,而带有不可比较性信息的问题往往却很复杂。而基于格蕴涵代数的格值逻辑能同时刻画可比较性信息和不可比较性信息。本文主要对格蕴涵代数的子结构以及基于格蕴涵代数的格值逻辑系统的多元α-语义归结自动推理展开研究。深入系统地刻画了格蕴涵代数的滤子理论与同余理论；给出了基于格蕴涵代数的格值逻辑系统的α-归结域的结构；以及在基于格值逻辑系统的多元α-归结自动推理基础上,借鉴基于经典逻辑的语义归结自动推理方法,给出了基于格值逻辑系统的多元α-语义归结自动推理的理论、方法、算法、程序。主要取得了以下四个方面的研究成果：第一部分,研究了基于格蕴涵代数的格值逻辑系统的语义代数—格蕴涵代数的模糊滤子理论与模糊同余理论。其一,引入了格蕴涵代数的极小素滤子、模糊素滤子、基于格上t-模T的LT-滤子以及基于区间值t-模丁的区间值丁-模糊滤子；分别给出了极小素滤子与模糊素滤子的性质、结构以及等价刻画；得到了LT-滤子的若干性质及等价刻画；给出了区间值T-模糊滤子的性质并分析了几类区间值T-模糊滤子的关系。其二,分别建立了格蕴涵代数的模糊同余理论、基于格上t-模T的LT-同余理论以及基于区间值t-模丁的区间值T-模糊同余理论；刻画了这几类模糊同余关系的性质；得到了由这几类模糊同余关系诱导的商格蕴涵代数以及同态定理。这将为格值逻辑系统中广义文字的α-归结域的结构研究奠定基础。第二部分,研究了基于格蕴涵代数的格值逻辑系统的α-归结域的结构。在基于格值逻辑系统的多元α-归结原则的基础上,建立了基于格值逻辑系统的a-归结域的代数结构。给出了基于格值逻辑系统的任意3个广义文字(所含蕴涵算子的个数不超过2)的α-可归结性的判定。这将为基于格值逻辑系统的多元α-归结方法的研究奠定基础。第三部分,首先进一步深入研究了基于格蕴涵代数的格值命题逻辑系统LP(X)的多元α-归结原理的基本理论,给出了在基于LP(X)的多元α-归结演绎中参与多元α-归结的广义文字个数随着归结演绎的推进而动态变化的基本原则；给出了基于LP(X)的可多元a-归结式集合的代数结构；并对基于LP(X)的多元a-归结原理的有效性进行了一定分析；这为建立基于LP(X)的多元α-语义归结方法建立了理论基础。其次,基于LP(X)的多元a-归结原理,建立了基于LP(X)的多元a-语义归结方法,给出了多元a-语义互撞、多元a-语义归结演绎的定义,并建立了基于LP(X)的多元α-语义归结方法的可靠性与条件完备性；并对基于LP(X)中多元α-语义归结方法的有效性进行了一定分析。最后,在LP(X)中,构造了一种基于LP(X)的多元α-语义归结算法,并以实例说明了该算法的正确性；证明了基于LP(X)的多元a-语义归结算法的可靠性与完备性；并对基于LP(X)中多元α-语义归结自动推理算法的复杂性与有效性进行了一定分析；设计了基于LP(X)的多元语义归结自动推理程序。第四部分,首先,进一步深入研究了基于格蕴涵代数的格值一阶逻辑系统LF(X)的多元α-归结原理的基本理论,给出了在基于LF(X)的多元α-归结演绎中参与多元α-归结的广义文字个数随着归结演绎的推进而动态变化的基本原则；给出了LF(X)的多元α-归结的下降引理与等价转换定理；对基于LF(X)的多元α-归结原理的有效性进行了一定分析；这为建立基于LF(X)的多元a-语义归结方法与算法建立了理论基础。其次,基于LF(X)的多元α-归结原理,将基于LP(X)的多元α-语义归结方法扩展至LF(X),建立了基于LF(X)的多元α-语义归结方法,给出了多元α-语义互撞、多元α-语义归结演绎的定义,并建立了基于LF(X)的多元α-语义归结方法的可靠性与条件完备性以及等价转换定理；并对基于LF(X)中多元α-语义归结方法的有效性进行了一定分析。最后,在LF(X)中,构造了一种基于LF(X)的多元α-语义归结自动推理算法及实现；给出了基于LF(X)的多元α-语义归结算法的可靠性与完备性；并以实例说明了该算法的有效性。