基于格值逻辑的α-锁归结与α-锁调解自动推理

The present project focuses on efficient α-lock resolution-based and α-lock paramodulation-based automated reasoning with heuristically dynamic indexing strategies, which includes their theories, approaches, algorithms and utility procedures for lattice-valued logic with equality. Fristly, the structure of generalized literals, the resolution field of some typical generalized literals, and the criterion for selecting number of resolved generalized literals are given. Secondly, heuristically dynamic indexing strategies for α-lock resolution and α-generalized lock resolution are proposed, the soundness and completeness of these resolution methods are established. Thridly, α-lock paramodulation automated reasoning for handling lattice-valued logical formulae with equality is proposed. The soundness and completeness of α-lock paramodulation method with heuristically dynamic indexing strategy are given. According to the above results, the automated reasoning algorithm and procedure for lattice-valued logic are contrived. This work may provide an effective support for automated reasoning scheme in lattice-valued logic based on lattice implication algebra with the aim at establishing theoritical foundation and practical tools for mechanical theorem proving, formal verification and some other fields.

本项目围绕带等词的格值逻辑系统，研究启发式动态配锁策略下的α-锁归结与α-锁调解自动推理理论、方法和算法，设计相应的自动推理程序。主要内容包括：一、研究格值命题逻辑系统中广义文字的结构、典型类广义文字的归结域及其归结文字个数的选择。二、针对α-锁归结与α-广义锁归结方法，提出启发式动态配锁策略。在该策略下，分别建立两种锁归结方法的可靠性与完备性。三、针对带等词的逻辑公式，建立基于格值一阶逻辑的α-锁调解自动推理理论和方法，并建立该调解方法在启发式动态配锁策略下的可靠性与完备性。四、针对上述理论和方法，设计基于格值逻辑的自动推理程序。项目预期的成果有望为基于格值逻辑的自动推理研究提供新的思路，为定理机器证明、形式化验证等应用方面提供理论基础和实用工具。

为处理含不确定性特别是不可比较性的信息提供了有效工具，本项目基于格值逻辑系统与自动推理理论，针对带等词的格值逻辑公式，建立了高效的α-（广义）锁归结和α-锁调解自动推理理论和方法，设计了相应的自动推理程序。研究成果主要包括以下三个方面：. 基于格值逻辑的广义文字的结构及其α-可归结性的研究。具体为：给出了L_6P(X)上逻辑公式的性质，并得到了该逻辑系统中判断公式是否为k阶IESF的规则。进一步地，得到了寻找所有k阶IESF的统一算法。给出了基于格值命题逻辑LP(X)的多元α-归结式集合的代数结构，以及3个广义文字的α-可归结性的判定方法。给出了LP(X)中多元α-归结演绎中参与多元-归结的广义文字个数随归结演绎动态变化的基本原则。. 基于格值逻辑的α-（广义）锁归结、α-锁调解理论与方法的研究。具体为：建立了基于格值逻辑的多元α-语义归结、α-准锁语义归结、α-半锁语义归结、α-群锁归结、非子句多元α-有序线性广义归结、α-有序（线性）极小归结和α-有序语义归结自动推理理论与方法，包括其可靠性、完备性及其相容性。给出了基于格值逻辑的合适归结水平集，证明了在合适归结水平下等词公理与E解释的等价性，以及逻辑公式不可满足性的等价转换。提出了α-调解原理与的概念，建立了α-调解原理的可靠性与完备性。给出了基于格值逻辑的α-GH调解的定义，证明了α-GH调解的可靠性与完备性。 . 基于格值逻辑的实用证明器的实现。具体为：选择典型的格值命题逻辑系统，设计了相应的证明器。验证了一批格值逻辑公式，初步显现了α-锁归结和α-锁调解自动推理方法的优势。进一步地，将研究成果推广至经典二值逻辑中，并形成了多个基于二值逻辑的自动定理证明器。利用这些证明器证明了TPTP问题库、Mizar问题库中25万余个定理，特别是证明了rating 1的定理（其它证明器均未能成功证明）69个，初步显现证明器的能力。这为定理机器证明、形式化验证等应用方面提供理论基础和应用工具。