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
    Abraham, Ajith
    Corchado, Emilio
    Corchado, Juan M.
    [J]. NEUROCOMPUTING, 2009, 72 (13-15) : 2729 - 2730
  • [2] [Anonymous], 2003, STUD FUZZINESS SOFT
  • [3] Hybrid intelligent algorithms and applications
    Corchado, Emilio
    Abraham, Ajith
    de Carvalho, Andre
    [J]. 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
    Liu, J
    Ruan, D
    Xu, Y
    Song, ZM
    [J]. 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)
    Ma, Jun
    Li, Wenjiang
    Ruan, Da
    Xu, Yang
    [J]. INFORMATION SCIENCES, 2007, 177 (04) : 1046 - 1062
  • [8] PEI Z, 2009, LINGUISTIC VALUES BA
  • [9] A MACHINE-ORIENTED LOGIC BASED ON RESOLUTION PRINCIPLE
    ROBINSON, JA
    [J]. JOURNAL OF THE ACM, 1965, 12 (01) : 23 - &
  • [10] Wang GJ., 2006, Introduction to mathematical logic and resolution principle (In Chinese)
12