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

项目名称： 基于格值逻辑的α-锁归结与α-锁调解自动推理

项目编号： No.61305074

项目类型： 青年科学基金项目

立项/批准年度： 2014

项目学科： 自动化技术、计算机技术

项目作者： 何星星

作者单位： 西南交通大学

项目金额： 22万元

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

中文关键词： 格值逻辑；α-自动推理；α-锁归结；α-锁调解；启发式策略

英文摘要： 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.

英文关键词： Lattice valued logic；α-Automated reasoning；α-Lock resolution；α-Lock paramodulation；Heuristic Searching strategies