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

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.

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

为了处理带有不可比较性信息的自动推理，在基于格蕴涵代数的格值命题逻辑系统LP(X)中，建立了α-群锁语义归结自动推理方法及其可靠性与条件完备性，进一步将该方法拓展到了相应的格值一阶逻辑系统LF(X)中，并基于LF(X)证明了该方法的可靠性定理、提升引理与条件完备性定理。同时，分别将语言真值格值命题逻辑LV(n×2)P(X)与一阶逻辑LV(n×2)F(X)中的α-群归结原理、α-群锁语义归结等价转化到了一个更简单的格值命题逻辑LVnP(X)中。此外，基于格值命题逻辑LnP(X)给出了一些α-群归结组的判定原则。这为进一步将语言真值α-归结自动推理用于实际问题提供了一定的理论基础。