格值一阶逻辑系统的α广义归结原理

doi:10.3969/j.issn.1001-2400.2014.01.024

Abstract

Abstract:

In the framework of the lattice-valued logic system based on the lattice implication algebra, the α-resolution principle based on the lattice-valued logic system is extended from generalized clauses set to general generalized clauses set. In this paper, the α-generalized resolution principle is presented in the lattice-valued first-order logic system LF(X). At the same time, the soundness theorem is established in LF(X). By using the lift lemma, the weak completeness theorem is also proved. This work can provide a new automated reasoning technology in order to establish novel generalized resolution methods for lattice-valued logic systems.

Key words: lattice-valued first-order logic, general generalized clause, local extremely complex generalized literal, generalized resolution, automated reasoning

XU Weitao;ZHANG Wenqiang;XU Yang;ZHANG Dexian. α-generalized resolution principle based on the lattice-valued first-order logic system[J].J4, 2014, 41(1): 135-139.

References

［1］ Robinson J P. A Machine-Oriented Logic Based on the Resolution Principle［J］. Journal of ACM, 1965, 12(1): 23-41.
［2］ Chang C L, Lee R C T. Symbolic Logic and Mechanical Theorem Proving ［M］. New York: Academic Press, 1973.
［3］ Wos L. Automated Reasoning: 33 Basic Research Problems［M］. Englewood Cliffs: Prentice Hall, 1988.
［4］ Xu Y, Ruan D, Qin K Y, et al. Lattice-Valued Logic—an Alternative Approach to Treat Fuzziness and Incomparability ［M］. New York: Springer-Verlag, 2003.
［5］ Sofronie-Stokkermans V. Automated Theorem Proving by Resolution in Non-Classical Logics ［J］. Annals of Mathematics and Artificial Intelligence, 2007, 49(1-4): 221-252.
［6］ Riva A, Nuzzo A, Stefanelli M, et al. An Automated Reasoning Framework for Translational Research ［J］. Journal of Biomedical Informatics, 2010, 43(3): 419-427.
［7］ Lu Zhirui, Augusto J, Liu Jun, et al. A Linguistic Truth-Value Temporal Reasoning(LTR) System and Its Application to the Design of an Intelligent Environment ［J］. International Journal of Computational Intelligence Systems, 2012, 5(1): 173-196.
［8］王湘浩, 刘叙华. 广义归结［J］. 计算机学报, 1982, 5(2): 81-92.
Wang Xianghao, Liu Xuhua. Generalized resolution ［J］. Chinese Journal of Computers, 1982, 5(2): 81-92.
［9］刘叙华. 基于归结方法的自动推理［M］. 北京: 科学出版社, 1994.
［10］徐扬. 格蕴涵代数［J］. 西南交通大学学报, 1993, 89(1): 20-27.
Xu Yang. Lattice Implication Algebra ［J］. Journal of Southwest Jiaotong University, 1993, 89(1): 20-27.
［11］ Xu Y, Liu J, Song Z M, et al. On Semantics of L-Valued First-Order Logic L_vft［J］. International Journal General Systems, 2000, 29(1): 53-79.
［12］ 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.
［13］ 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.
［14］ 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.
［15］徐扬. 基于格值逻辑的语言真值α-广义归结自动推理研究［J］. 学术动态(西南交通大学), 2009, (4): 1-12.
Xu Yang. Linguistic Truth-valued α-generalized Resolution Automated Reasoning Research Based on Lattice-valued Logic ［J］. Xushu Dongtai(Southwest Jiaotong University), 2009, (4): 1-12.
［16］ Xu Y, Xu W T, Zhong X M, et al. α-Generalized Resolution Principle Based on Lattice-valued Propositional Logic LP(X) ［C］//Proceedings of the 9th International FLINS Conference. Singapore: World Scientific Publishing, 2010: 66-71.

α-generalized resolution principle based on the lattice-valued first-order logic system

PDF (PC)

Like

Knowledge

Abstract

Cite this article

share this article

References

Related Articles 0

Metrics

Comments

Recommended 10