四值非链格值命题逻辑系统LP_4(X)的归结原理

Resolution Principle Based on Four-element Non-Chain Lattice-valued Proposition Logic LP_4(X)

基于格蕴涵代数的格值命题逻辑系统LP4(X)的相关概念和结果,给出了LP4(X)上的归结原理,并证明了其可靠性和完备性.四值命题逻辑系统LP4(X)作为含有不可比真值的一种基本且重要的格蕴涵代数结构,其上归结原理的研究为归结算法的实现提供了理论基础,从而为处理含有不可比真值的格值逻辑系统在智能推理系统中的实际应用提供了有力的支持.

The resolution principle based on fourelement nonchain latticevalued logic LP4(X) is investigated and sound theorem and complete theorem of this resolution principle proved. Fourelement nonchain latticevalued logic LP4(X) as a fundamental and important lattice implication algebra which includes incomparable element, resolution based on LP4(X) will be the theoretical foundation of resolution algorithm. Accordingly, this paper will help support the application of intelligent reasoning system including incomparable element based on latticevalued logic.