Journal of shanghai Jiaotong University (Science) ›› 2012, Vol. 17 ›› Issue (2): 178-181.doi: 10.1007/s12204-012-1249-1

• Articles • Previous Articles     Next Articles

Ideal Resolution Principle for Lattice-Valued First-Order Logic Based on Lattice Implication Algebra

Ideal Resolution Principle for Lattice-Valued First-Order Logic Based on Lattice Implication Algebra

XU Wei-tao 1,3∗ (许伟涛), XU Yang 1,2(徐扬)   

  1. (1. Intelligent Control Development Center, Southwest Jiaotong University, Chengdu 610031, China; 2. Department of Mathematics, Southwest Jiaotong University, Chengdu 610031, China; 3. College of Information Science and Engineering, Henan University of Technology, Zhengzhou 450001, China)
  2. (1. Intelligent Control Development Center, Southwest Jiaotong University, Chengdu 610031, China; 2. Department of Mathematics, Southwest Jiaotong University, Chengdu 610031, China; 3. College of Information Science and Engineering, Henan University of Technology, Zhengzhou 450001, China)
  • Online:2012-04-28 Published:2012-05-31

Abstract: As a continuate work, ideal-based resolution principle for lattice-valued first-order logic system LF(X) is proposed, which is an extension of α-resolution principle in lattice-valued logic system based on lattice implication algebra. In this principle, the resolution level is an ideal of lattice implication algebra, instead of an element in truth-value field. Moreover, the soundness theorem is given. In the light of lifting lemma, the completeness theorem is established. This can provide a new tool for automated reasoning.

Key words:

automated reasoning| lattice-valued logic| lattice implication algebra| generalized clause

摘要: As a continuate work, ideal-based resolution principle for lattice-valued first-order logic system LF(X) is proposed, which is an extension of α-resolution principle in lattice-valued logic system based on lattice implication algebra. In this principle, the resolution level is an ideal of lattice implication algebra, instead of an element in truth-value field. Moreover, the soundness theorem is given. In the light of lifting lemma, the completeness theorem is established. This can provide a new tool for automated reasoning.

关键词:

automated reasoning| lattice-valued logic| lattice implication algebra| generalized clause

CLC Number: