基于格值一阶逻辑LF（X）的多元α-归结原理的注记

摘要

进一步深入研究了基于格蕴涵代数的格值一阶逻辑系统 LF(X )的多元α-归结原理的基本理论，给出了在基于 LF(X )的多元α-归结演绎中参与多元α-归结的广义文字个数随着归结演绎的推进而动态变化的基本原则。对基于 LF(X )的多元α-归结原理的有效性进行了一定分析；这为建立基于 LF(X )的多元α-归结方法以及构造多元α-归结算法建立了理论基础。%The relative theory of multi-ary α-resolution principle based on lattice-valued first-order logical system LF ( X ) is further investigated, the basic principle of the number of generalized literals which take part in the multi-ary α-resolution varies with the resolution deduction in LF(X ) . The validities of multi-ary α -resolution principle in LF(X ) are ana-lyzed, which will lay the theoretical foundation for the multi-ary α-semantic resolution method in LF(X ) .