a-Generalized Linear Resolution Method Based on Lattice-Valued First-Order Logic System
As a continuation of research work on a-generalized resolution for lattice-valued logic system, the ageneralized linear resolution method for latticevalued first-order logic system LF(X) based on lattice implication algebra is presented, which can provide an automated reasoning tool for information processing and knowledge representation. The soundness theorem is established. By use of the lifting lemma, the weak completeness theorem is also investigated in lattice-valued first-order logic system. Additional, on the basis of the present method for lattice.valued first-order logic system LF (X), an a-generalized linear resolution automated reasoning algorithm is designed.
automated reasoning lattice implication algebra lattice-valued logic generalized linear resolution general g-clause
Weitao Xu Yang Xu
Intelligent Control Development Center Southwest Jiaotong University Chengdu 610031, China College of Maths Southwest Jiaotong University Chengdu 610031, China
国际会议
重庆
英文
720-724
2011-08-20（万方平台首次上网日期，不代表论文的发表时间）