%A XU Wei-tao 1,3 (许伟涛), XU Yang 1,2(徐扬)
%T Ideal Resolution Principle for Lattice-Valued First-Order Logic Based on Lattice Implication Algebra
%0 Journal Article
%D 2012
%J J Shanghai Jiaotong Univ Sci
%R 10.1007/s12204-012-1249-1
%P 178-181
%V 17
%N 2
%U {https://xuebao.sjtu.edu.cn/sjtu_en/CN/abstract/article_42105.shtml}
%8 2012-04-28
%X 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.