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

doi:10.3969/j.issn.1001-2400.2014.01.024

J4 ›› 2014, Vol. 41 ›› Issue (1): 135-139.doi: 10.3969/j.issn.1001-2400.2014.01.024

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

许伟涛¹;张闻强¹;徐扬²;张德贤¹

(1. 河南工业大学信息科学与工程学院，河南郑州 450001；
2. 西南交通大学数学学院，四川成都 610031)

收稿日期:2012-11-08 出版日期:2014-02-20 发布日期:2014-04-02
通讯作者: 许伟涛
作者简介:许伟涛(1979-)，男，讲师，博士，E-mail: hnxmxwt@163.com．
基金资助:
国家自然科学基金资助项目(61175055)；国家自然科学青年基金资助项目(61300123)；国家高技术研究发展计划(863计划)资助项目(2012AA101608)；河南省教育厅自然科学资助项目(13B520945)；河南工业大学高层次人才基金资助项目(2012BS012)

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

XU Weitao¹;ZHANG Wenqiang¹;XU Yang²;ZHANG Dexian¹

(1. College of Information Science and Engineering, Henan Univ. of Technology, Zhengzhou 450001， China;
2. School of Mathematics, Southwest Jiaotong Univ., Chengdu 610031， China)

Received:2012-11-08 Online:2014-02-20 Published:2014-04-02
Contact: XU Weitao

摘要/Abstract

摘要：

在基于格蕴涵代数的格值逻辑系统框架下，笔者扩展了基于格值逻辑系统的α归结原理，将广义子句集上的归结扩展到一般广义子句集上，提出了基于格值一阶逻辑系统LF(X)的α广义归结原理，建立了格值一阶逻辑系统中α广义归结原理的可靠性定理．通过给出的提升引理，证明了该原理的弱完备性定理．这将为建立基于格值逻辑系统的广义归结方法提供新的自动推理技术．

关键词: 格值一阶逻辑, 一般广义子句, 局部极复杂广义文字, 广义归结, 自动推理

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

许伟涛;张闻强;徐扬;张德贤. 格值一阶逻辑系统的α广义归结原理[J]. J4, 2014, 41(1): 135-139.

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.

参考文献

［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)

赞

可视化

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 0

Metrics

本文评价

推荐阅读 10