α-Generalized lock resolution method in linguistic truth-valued lattice-valued logic

被引：8
作者：
He, Xingxing [1 ]
Xu, Yang [1 ]
Liu, Jun [2 ]
Chen, Shuwei [2 ]
机构：
[1] SW Jiaotong Univ, Intelligent Control Dev Ctr, Chengdu 610031, Sichuan, Peoples R China
[2] Univ Ulster, Sch Comp & Math, Coleraine BT52 1SA, Londonderry, North Ireland
来源：
INTERNATIONAL JOURNAL OF COMPUTATIONAL INTELLIGENCE SYSTEMS | 2012年 / 5卷 / 06期
基金：
中国国家自然科学基金;
关键词：
Non-clausal resolution; alpha-Generalized lock resolution; alpha-Generalized linear semi-lock resolution; Linguistic truth-valued lattice-valued logic; Lattice implication algebras; 1ST-ORDER LOGIC; PRINCIPLE; LP(X); STRATEGY; ORDER; LF(X);
D O I：
10.1080/18756891.2012.747665
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
This paper focuses on e fficient non-clausal resolution-based automated reasoning methods and algorithms for a lattice-ordered linguistic truth-valued logic, which corresponds to extensions of alpha-lock resolution. Firstly, alpha-generalized lock resolution is proposed for lattice-valued propositional logic and first order logic, respectively, along with their concepts, soundness and completeness. Then, alpha-generalized lock resolution for first order linguistic truth-valued lattice-valued logic LV(nx2)F(X) is equivalently transformed into that for propositional logic LnP(X), which can greatly reduce the complexity of the resolution procedure. Finally, alpha-generalized linear semi-lock resolution is discussed, and its general algorithm is also contrived. This work provides more efficient and natural resolution automated reasoning scheme in linguistic truth-valued logic based on lattice implication algebra with the aim at establishing formal tools for symbolic natural language processing.
引用
收藏
页码：1120 / 1134
页数：15
相关论文
共 38 条
[1]   Reductions for non-clausal theorem proving [J].
Aguilera, G ;
de Guzmán, IP ;
Ojeda-Aciego, M ;
Valverde, A .
THEORETICAL COMPUTER SCIENCE, 2001, 266 (1-2) :81-112
[2]  
[Anonymous], 2003, STUD FUZZINESS SOFT
[3]   Resolution with Order and Selection for Hybrid Logics [J].
Areces, Carlos ;
Gorin, Daniel .
JOURNAL OF AUTOMATED REASONING, 2011, 46 (01) :1-42
[4]  
Boyer R. S., 1971, Ph.D. Thesis
[5]   Resolution for temporal logics of knowledge [J].
Dixon, C ;
Fisher, M ;
Wooldridge, M .
JOURNAL OF LOGIC AND COMPUTATION, 1998, 8 (03) :345-372
[6]   On compatibilities of α-lock resolution method in linguistic truth-valued lattice-valued logic [J].
He, Xingxing ;
Xu, Yang ;
Liu, Jun ;
Chen, Shuwei .
SOFT COMPUTING, 2012, 16 (04) :699-709
[7]   α-Lock resolution method for a lattice-valued first-order logic [J].
He, Xingxing ;
Xu, Yang ;
Liu, Jun ;
Ruan, Da .
ENGINEERING APPLICATIONS OF ARTIFICIAL INTELLIGENCE, 2011, 24 (07) :1274-1280
[8]   On α-satisfiability and its α-lock resolution in a finite lattice-valued propositional logic [J].
He, Xingxing ;
Liu, Jun ;
Xu, Yang ;
Martinez, Luis ;
Ruan, Da .
LOGIC JOURNAL OF THE IGPL, 2012, 20 (03) :579-588
[9]   Using resolution for testing modal satisfiability and building models [J].
Hustadt, U ;
Schmidt, RA .
JOURNAL OF AUTOMATED REASONING, 2002, 28 (02) :205-232
[10]   A resolution-like strategy based on a lattice-valued logic [J].
Liu, J ;
Ruan, D ;
Xu, Y ;
Song, ZM .
IEEE TRANSACTIONS ON FUZZY SYSTEMS, 2003, 11 (04) :560-567
1234