General form of a-Linear Resolution Method based on Lattice-Valued First-Order Logic System

摘要：

In this paper we propose a new resolution approach for automated reasoning in artificial intelligence. The general form o-linear resolution method is established in lattice-valued first-order logic system LF(X) based on lattice implication algebra. The soundness theorem is given in LF(X). By using lift lemma, the weak completeness theorem is also investigated in LFX). This method is to provide a scientific and efficient reasoning tool for theorem proving based on lattice-valued logic system.

关键词： automated reasoning lattice-valued first-order logic general form of a-linear resolution generalized clause generalized literal

作者: Weitao Xu Wenqiang Zhang Yang Xu

作者单位: College of Information Science and Engineering, Henan University of Technology, Zhengzhou 450001, Ch Department of Mathematics, Southwest Jiaotong University, Chengdu 610031, China

会议类型: 国际会议

会议名称: 2012 Fifth International Symposium on Computational Intelligence and Design 第五届计算智能与设计国际会议 ISCID 2012

会议地点: 杭州

会议语种:英文

页码: 864-867

在线出版日期: 2012-10-28（万方平台首次上网日期，不代表论文的发表时间）