摘要
进一步深入研究了基于格蕴涵代数的格值一阶逻辑系统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 analyzed, which will lay the theoretical foundation for the multi-ary α-semantic resolution method in LF（X）.
出处
《计算机工程与应用》
CSCD
北大核心
2015年第14期51-56,190,共7页
Computer Engineering and Applications
基金
国家自然科学基金(No.61175055
No.61305074)
四川省教育厅科研项目重点项目(No.14ZA0245)
教育部"数学与应用数学"专业综合改革(No.ZG0464)
四川省教育厅"数学与应用数学"专业综合改革(No.01249)
四川省教育厅科研项目(No.14ZA0245)
四川省应用基础研究计划(No.2015JY0120)
关键词
格蕴涵代数
格值一阶逻辑
多元α-归结原理
lattice implication algebras
lattice-valued first-order logic
multi-ary α-resolution principle
