Resolution based on six lattice-valued proposition logic LP6(X)

被引：0
作者：
Meng, D [1 ]
Wang, XF [1 ]
Xu, Y [1 ]
Qin, KY [1 ]
机构：
[1] SW Jiaotong Univ, Intelligent Control Dev Ctr, Sichuan, Chengdu, Peoples R China
来源：
2003 IEEE INTERNATIONAL CONFERENCE ON SYSTEMS, MAN AND CYBERNETICS, VOLS 1-5, CONFERENCE PROCEEDINGS | 2003年
关键词：
artificial intelligence; multi-valued logic; lattice-valued logic; automated reasoning; resolution;
D O I：
暂无
中图分类号：
TP [自动化技术、计算机技术];
学科分类号：
0812 ;
摘要：
Resolution-based automated reasoning theory is an important and active research field in artificial intelligence. It is used to judge the satisfiability of any logic formula. With the development of classical and non-classical logic, the resolution theory and method based on different logic system has been discussed widely and deeply. In the present paper, a new resolution principle by by using ultrafilter in LP6(X) is put for-ward. Different from existed method of resolution.. this resolution in this paper is based on ultrafilter of lattice implication algebra. In this paper, resolution principle based on any formula is discussed and soundness theorem is proved. Subsequently, algorithm of this resolution based on ultrafilter is given. Because of LP6(X) is a non-chain, non-boolean and non-well-ordered algebra structure, resolution based on LP6(X) will be the theoretical foundation of resolution on lattice-valued truth-field. Accordingly, the research in this paper will be helpful support for the application of intelligent reasoning system based on lattice-valued logic.
引用
收藏
页码：2489 / 2494
页数：6
相关论文
共 50 条
[41]   α-Lock paramodulation for lattice-valued propositional logic [J].
He, Xingxing ;
Xu, Yang ;
Liu, J. .
2015 10TH INTERNATIONAL CONFERENCE ON INTELLIGENT SYSTEMS AND KNOWLEDGE ENGINEERING (ISKE), 2015, :18-20
[42]   Progress and prospect in lattice-valued logic systems based on lattice implication algebras [J].
Xu, Y ;
Ruan, D ;
Liu, J .
APPLIED COMPUTATIONAL INTELLIGENCE, 2004, :29-34
[43]   Ultraproduct of first-order lattice-valued logic LF(X) based on finite lattice implication algebra [J].
Wang Xuefang ;
Liu Peishun .
INTERNATIONAL JOURNAL OF COMPUTER SCIENCE AND NETWORK SECURITY, 2006, 6 (5A) :195-200
[44]   A model for handling linguistic terms in the framework of lattice-valued logic LF(X) [J].
Ma, J ;
Li, WJ ;
Xu, Y ;
Song, ZM .
2004 IEEE INTERNATIONAL CONFERENCE ON SYSTEMS, MAN & CYBERNETICS, VOLS 1-7, 2004, :1504-1509
[45]   General form of α-Linear Resolution Method based on Lattice-Valued First-Order Logic System [J].
Xu, Weitao ;
Zhang, Wenqiang ;
Xu, Yang .
2012 FIFTH INTERNATIONAL SYMPOSIUM ON COMPUTATIONAL INTELLIGENCE AND DESIGN (ISCID 2012), VOL 2, 2012, :286-289
[46]   Non-Clausal Multi-ary α-Generalized Resolution Calculus for a Finite Lattice-Valued Logic [J].
Xu, Yang ;
Liu, Jun ;
He, Xingxing ;
Zhong, Xiaomei ;
Chen, Shuwei .
INTERNATIONAL JOURNAL OF COMPUTATIONAL INTELLIGENCE SYSTEMS, 2018, 11 (01) :384-401
[47]   On Compactness and Consistency in Finite Lattice-Valued Propositional Logic [J].
Pan, Xiaodong ;
Xu, Yang ;
Martinez, Luis ;
Ruan, Da ;
Liu, Jun .
HYBRID ARTIFICIAL INTELLIGENCE SYSTEMS, PT 2, 2010, 6077 :328-+
[48]   Graded method of lattice-valued logic based on MV-algebra semantics [J].
Zuo, W.-B. (zuoweibing@ncwu.edu.cn), 1600, Chinese Institute of Electronics (41) :2035-2040
[49]   L-TAUTOLOGY THEORY IN LATTICE-VALUED PROPOSITIONAL LOGIC [J].
Pan, Xiaodong ;
Xu, Kaijun ;
Qin, Keyun ;
Xu, Yang .
COMPUTATIONAL INTELLIGENCE: FOUNDATIONS AND APPLICATIONS: PROCEEDINGS OF THE 9TH INTERNATIONAL FLINS CONFERENCE, 2010, 4 :105-+
[50]   Non-clausal Multi-ary α-Generalized Resolution Principle for a Lattice-valued First-Order Logic [J].
Xu, Yang ;
Liu, Jun ;
He, Xingxing ;
Zhong, Xiaomei ;
Chen, Shuwei .
2015 10TH INTERNATIONAL CONFERENCE ON INTELLIGENT SYSTEMS AND KNOWLEDGE ENGINEERING (ISKE), 2015, :1-7
12345