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

详细信息    查看全文 | 推荐本文 |

英文篇名：α-generalized resolution principle based on the lattice-valued first-order logic system 作者：许伟涛 ; 张闻强 ; 徐扬 ; 张德贤 英文作者：XU Weitao;ZHANG Wenqiang;XU Yang;ZHANG Dexian;College of Information Science and Engineering,Henan Univ.of Technology;School of Mathematics,Southwest Jiaotong Univ.; 关键词：格值一阶逻辑 ; 一般广义子句 ; 局部极复杂广义文字 ; 广义归结 ; 自动推理 英文关键词：lattice-valued first-order logic;;general generalized clause;;local extremely complex generalized literal;;generalized resolution;;automated reasoning 中文刊名：XDKD 英文刊名：Journal of Xidian University 机构：河南工业大学信息科学与工程学院;西南交通大学数学学院; 出版日期：2013-09-16 09:26 出版单位：西安电子科技大学学报 年：2014 期：v.41 基金：国家自然科学基金资助项目(61175055);; 国家自然科学青年基金资助项目(61300123);; 国家高技术研究发展计划(863计划)资助项目(2012AA101608);; 河南省教育厅自然科学资助项目(13B520945);; 河南工业大学高层次人才基金资助项目(2012BS012) 语种：中文; 页：XDKD201401025 页数：4 CN：01 ISSN：61-1076/TN 分类号：141-143+145

摘要

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

引文

[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:33Basic 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 Lvft[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.