基于格值逻辑的α-n(t)元归结动态自动推理研究

针对带有不可比较性信息的自动推理，依据基于格蕴涵代数的格值逻辑系统，借鉴基于经典二值逻辑的0-2元归结自动推理的学术思想，在基于格蕴涵代数的格值逻辑的α-2元归结自动推理研究基础上，分别建立基于格值命题逻辑LP(X)和格值一阶逻辑LF(X)、格值分层、群组归结、动态演绎、效率提高、从本质上发展归结自动推理的α-n(t)元归结动态自动推理具有可靠性与完备性的理论、方法、算法和程序。

针对带有不可比较性信息的自动推理，在基于格蕴涵代数的格值逻辑系统中，于α-n(t)元归结动态自动推理理论、方法、算法和程序方面取得如下主要结果，这将为处理带有不可比较性信息的自动推理研究与应用提供基础及手段。.在格值命题逻辑LP(X)中：建立了子句型和非子句型的α-n(t)元归结动态自动推理理论，给出了α-n(t)元归结演绎中广义文字个数动态变化的基本原则、α-n(t)元可归结式集合的结构；建立了α-极小归结、α-有序线性归结和α-广义语义归结；在语言真值格值逻辑中建立了α-广义锁归结理论。提出了α-n(t)元语义归结方法，构造了算法，设计了程序；建立了非子句α-n(t)元有序线性广义归结方法；建立了α-有序线性极小归结方法、α-半锁语义归结方法、α-n(t)元锁归结方法、α-n(t)元准锁语义归结方法、α-n(t)元语义归结方法，在(Ln×L2)P(X)中构造了α-n(t)元准锁语义归结算法；基于LV(n×2)P(X)提出了α-线性归结方法并构造了算法；设计了α-有序线性归结算法；基于语言真值格值逻辑，提出了α-广义锁归结自动推理方法；建立了α-广义线性半锁归结方法，构造了算法。在L2P(X)中形成了0-n(t)元归结动态自动推理方法、算法、程序雏形，基于此形成了C程序验证工具Scavel C初级版，并已用于航空航天、武器装备、轨道交通等领域，验证程序150多万行，为完善C程序初现其独有作用。.在格值一阶逻辑LF(X)中：建立了子句型和非子句型α-n(t)元归结动态自动推理理论；给出了α-n(t)元归结演绎中广义文字个数动态变化的基本原则；建立了α-极小归结原理、基于理想的归结原理和α-广义归结原理；在 (Ln×L2)F(X)中，将α-归结原理的一般形式等价转化到了LnP(X)中。建立了α-n(t)元语义归结动态自动推理方法，构造了算法，并指出：可将LP(X)的α-n(t)元语义归结自动推理程序应用于LF(X)的α-n(t)元语义归结自动推理；提出了α-有序线性归结，构造了算法；建立了非子句α-n(t)元有序线性广义归结方法；建立了α-n(t)元准锁语义归结方法；建立了α-广义线性半锁归结方法，构造了算法；针对L9x2F(X)设计了α-语义归结自动推理程序；在L2F(X)中形成了0-n(t)元归结动态自动推理方法、算法、程序雏形，基于此已证明4800多个定理。