On α-satisfiability and its α-lock resolution in a finite lattice-valued propositional logic

被引：14

作者：

He, Xingxing ^{[1
]}

Liu, Jun ^{[2
]}

Xu, Yang ^{[1
]}

Martinez, Luis ^{[3
]}

Ruan, Da ^{[4
,5
]}

机构：

[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

[3] Univ Jaen, Dept Comp, E-23071 Jaen, Spain

[4] Univ Ghent, B-9000 Ghent, Belgium

[5] Belgian Nucl Res Ctr SCK CEN, B-2400 Mol, Belgium

来源：

LOGIC JOURNAL OF THE IGPL | 2012年 / 20卷 / 03期

基金：

中国国家自然科学基金;

关键词：

Lattice-valued logic; alpha-resolution principle; alpha-satisfiability; alpha-lock resolution method; finite lattice-valued propositional logic; PRINCIPLE; LP(X);

D O I：

10.1093/jigpal/jzr007

中图分类号：

O29 [应用数学];

学科分类号：

070104 ;

摘要：

Automated reasoning issues are addressed for a finite lattice-valued propositional logic LnP(X) with truth-values in a finite lattice-valued logical algebraic structure-lattice implication algebra. We investigate extended strategies and rules from classical logic to LnP(X) to simplify the procedure in the semantic level for testing the satisfiability of formulas in LnP(X) at a certain truth-value level alpha (alpha-satisfiability) while keeping the role of truth constant formula played in LnP(X). We propose a lock resolution method at a certain truth-value level alpha (alpha-lock resolution) in LnP(X) and have proved its theorems of soundness and weak completeness, respectively. We provide more efficient resolution based automated reasoning in LnP(X) and key supports for alpha-resolution-based automated reasoning approaches and algorithms in lattice based linguistic truth-valued logic.

引用

页码：579 / 588

页数：10

共 15 条

[1] Hybrid learning machines [J].

Abraham, Ajith ;

Corchado, Emilio ;

Corchado, Juan M. .

NEUROCOMPUTING, 2009, 72 (13-15) :2729-2730

[2]

[Anonymous], 2003, STUD FUZZINESS SOFT

[3] Hybrid intelligent algorithms and applications [J].

Corchado, Emilio ;

Abraham, Ajith ;

de Carvalho, Andre .

INFORMATION SCIENCES, 2010, 180 (14) :2633-2634

[4]

He XX, 2010, LECT NOTES ARTIF INT, V6077, P320

[5] 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

[6]

LIU X, 1994, RESOLUTION BASED AUT

[7] Filter-based resolution principle for lattice-valued propositional logic LP(X) [J].

Ma, Jun ;

Li, Wenjiang ;

Ruan, Da ;

Xu, Yang .

INFORMATION SCIENCES, 2007, 177 (04) :1046-1062

[8]

PEI Z, 2009, LINGUISTIC VALUES BA

[9] A MACHINE-ORIENTED LOGIC BASED ON RESOLUTION PRINCIPLE [J].

ROBINSON, JA .

JOURNAL OF THE ACM, 1965, 12 (01) :23-&

[10]

Wang GJ., 2006, Introduction to mathematical logic and resolution principle (In Chinese)

← 1 2 →