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

doi:10.1007/s12204-012-1249-1

上海交通大学学报（英文版） ›› 2012, Vol. 17 ›› Issue (2): 178-181.doi: 10.1007/s12204-012-1249-1

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

XU Wei-tao^1,3∗ (许伟涛), XU Yang^1,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)

出版日期:2012-04-28 发布日期:2012-05-31

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

XU Wei-tao^1,3∗ (许伟涛), XU Yang^1,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.

关键词: generalized clause, automated reasoning, lattice-valued logic, lattice implication algebra

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

中图分类号:

TP 391

XU Wei-tao 1,3 (许伟涛), XU Yang 1,2(徐扬). Ideal Resolution Principle for Lattice-Valued First-Order Logic Based on Lattice Implication Algebra[J]. 上海交通大学学报（英文版）, 2012, 17(2): 178-181.

XU Wei-tao 1,3 (许伟涛), XU Yang 1,2(徐扬). Ideal Resolution Principle for Lattice-Valued First-Order Logic Based on Lattice Implication Algebra[J]. Journal of shanghai Jiaotong University (Science), 2012, 17(2): 178-181.

参考文献

[1] Robinson J A. A machine-oriented logic based on the resolution principle [J]. Journal of the Association for Computing Machinery, 1965, 12(1): 23-41.

[2] Luckham D. Refinement theorems in resolution theory [C]//Proceedings of IRIA Symposium Automatic Demonstration. Versailes, France: Spring-Verlag,

1968: 16-21.

[3] Chang C L, Lee R C-T. Symbolic logic and mechanical theorem proving [M]. New York: Academic Press,1973.

[4] Liu Xu-hua. Resolution-based automated reasoning [M]. Beijing: Science Press, 1994 (in Chinese).

[5] Wos L. Automated reasoning: 33 basic research problems [M]. New Jersey, USA: Prentice Hall, 1988.

[6] Morgan C G. A resolution principle for a class of many-valued logics [J]. Logique and Analyse, 1976,19(74-76): 311-339.

[7] Baaz M, Ferm¨uller C G. Resolution-based theorem proving for many valued logics [J]. Journal of Symbolic Computation, 1995, 19(4): 353-391.

[8] Xu Yang. Lattice implication algebras [J]. Journal of Southwest Jiaotong University, 1993, 28(1): 20-27 (in Chinese).

[9] Xu Y, Liu J, Song Z M, et al. On semantics of Lvalued first-order logic Lvfl [J]. International Journal of General Systems, 2000, 29(1): 53-79.

[10] Xu Y, Song Z M, Qin K Y, et al. Syntax of Lvalued first-order logic Lvfl [J]. International Journal of Multiple-Valued Logic, 2001, 7: 213-257.

[11] Xu Y, Ruan D, Qin K, et al. Lattice-valued logic: An alternative approach to treat fuzziness and incomparability [M]. Berlin: Springer-Verlag, 2003.

[12] Xu Y, Ruan D, Kerre E E, et al. α-resolution principle based on lattice-valued propositional logic LP(X)[J]. Information Sciences, 2000, 130(1-4): 195-223.

[13] Xu Y, Ruan D, Kerre E E, et al. α-Resolution principle based on first-order lattice-valued logic LF(X)[J]. Information Sciences, 2001, 132(1-4): 221-239.

[14] Xu W T, Xu Y, Deng W H, et al. Ideal-based resolution principle for lattice-valued propositional logic LP(X) [C]// Proceedings of the 4th International Intelligent

Systems and Knowledge Engineering Conference.Singapore: World Scientific, 2009: 601-606.

[15] Xu Y, Liu J, Ruan D, et al. Determination of α-resolution in lattice-valued first-order logic LF(X) [J].Information Sciences, 2011, 181(10): 1836-1862.

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

可视化

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 1

编辑推荐

Metrics

本文评价