基于格值逻辑的语言真值α-群锁语义归结自动推理研究

项目名称： 基于格值逻辑的语言真值α-群锁语义归结自动推理研究

项目编号： No.11526171

项目类型： 专项基金项目

立项/批准年度： 2016

项目学科： 数理科学和化学

项目作者： 钟小梅

作者单位： 西南交通大学

项目金额： 2.6万元

中文摘要： 针对带有不可比较性信息的自动推理，依据基于格蕴涵代数的格值逻辑系统，借鉴经典二值逻辑中语义归结和锁归结自动推理的学术思想，在基于格蕴涵代数的格值逻辑的语言真值α-归结自动推理研究基础上，进一步研究基于格值命题逻辑系统LP(X)与一阶逻辑系统LF(X)的语言真值α-群锁语义归结自动推理，提出相应的基本理论、并建立具有可靠性和完备性的方法。

中文关键词： 自动推理；定理机器证明；α-群锁语义归结；格值逻辑；

英文摘要： Aiming at automated reasoning with incomparability information, according to lattice-valued logical system based on lattice implication algebra, drawing lessons from the academic ideas of semantic resolution and lock resolution automated reasoning based on classical 2-valued logic, and based on linguistic truth-valued α-resolution-based automated reasoning in lattice-valued logic with truth-values in lattice implication algebra, this project will focus on studying linguistic truth-valued α-group lock semantic resolution automated reasoning based on lattice-valued propositional logic system LP(X) and first-order logic system LF(X). Concretely, it will propose the corresponding basic theory and establish the method with soundness and completeness.

英文关键词： Automated reasoning；Automated theorem proving；α-group lock semantic resolution；lattice-valued logic；