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
相关论文
共 50 条
  • [21] α-RESOLUTION OF GENERALIZED LITERALS FOR LATTICE-VALUED PROPOSITIONAL LOGIC LnP(X)
    Xu, Weitao
    Xu, Yang
    COMPUTATIONAL INTELLIGENCE: FOUNDATIONS AND APPLICATIONS: PROCEEDINGS OF THE 9TH INTERNATIONAL FLINS CONFERENCE, 2010, 4 : 174 - 179
  • [22] α-resolution principle based on lattice-valued propositional logic LP(X)
    Xu, Y
    Ruan, D
    Kerre, EE
    Liu, J
    INFORMATION SCIENCES, 2000, 130 (1-4) : 195 - 223
  • [23] α-resolution principle based on an intermediate element lattice-valued propositional logic
    Meng, D
    Xu, Y
    PROCEEDINGS OF THE 6TH JOINT CONFERENCE ON INFORMATION SCIENCES, 2002, : 89 - 91
  • [24] α-Group Quasi-Lock Semantic Resolution Method Based on Lattice-Valued Propositional Logic LP(X)
    Zhong, Xiaomei
    Xu, Yang
    JOURNAL OF MULTIPLE-VALUED LOGIC AND SOFT COMPUTING, 2014, 22 (4-6) : 581 - 598
  • [25] α-Lock resolution method for a lattice-valued first-order logic
    He, Xingxing
    Xu, Yang
    Liu, Jun
    Ruan, Da
    ENGINEERING APPLICATIONS OF ARTIFICIAL INTELLIGENCE, 2011, 24 (07) : 1274 - 1280
  • [26] On compatibilities of α-lock resolution method in linguistic truth-valued lattice-valued logic
    He, Xingxing
    Xu, Yang
    Liu, Jun
    Chen, Shuwei
    SOFT COMPUTING, 2012, 16 (04) : 699 - 709
  • [27] α-Generalized lock resolution method in linguistic truth-valued lattice-valued logic
    He, Xingxing
    Xu, Yang
    Liu, Jun
    Chen, Shuwei
    INTERNATIONAL JOURNAL OF COMPUTATIONAL INTELLIGENCE SYSTEMS, 2012, 5 (06): : 1120 - 1134
  • [28] α-Generalized lock resolution method in linguistic truth-valued lattice-valued logic
    Xingxing He
    Yang Xu
    Jun Liu
    Shuwei Chen
    International Journal of Computational Intelligence Systems, 2012, 5 : 1120 - 1134
  • [29] α-resolution principle based on lattice-valued modal propositional logic LMP(X)
    Li, WJ
    Xu, Y
    Ma, J
    6TH WORLD MULTICONFERENCE ON SYSTEMICS, CYBERNETICS AND INFORMATICS, VOL XVI, PROCEEDINGS: COMPUTER SCIENCE III, 2002, : 114 - 118
  • [30] On compatibilities of α-lock resolution method in linguistic truth-valued lattice-valued logic
    Xingxing He
    Yang Xu
    Jun Liu
    Shuwei Chen
    Soft Computing, 2012, 16 : 699 - 709
12345