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 条
  • [1] α-Satisfiability and α-Lock Resolution for a Lattice-Valued Logic LP(X)
    He, Xingxing
    Xu, Yang
    Li, Yingfang
    Liu, Jun
    Martinez, Luis
    Ruan, Da
    HYBRID ARTIFICIAL INTELLIGENCE SYSTEMS, PT 2, 2010, 6077 : 320 - +
  • [2] α-Lock paramodulation for lattice-valued propositional logic
    He, Xingxing
    Xu, Yang
    Liu, J.
    2015 10TH INTERNATIONAL CONFERENCE ON INTELLIGENT SYSTEMS AND KNOWLEDGE ENGINEERING (ISKE), 2015, : 18 - 20
  • [3] Syntax theory of finite lattice-valued propositional logic
    XiaoDong Pan
    Dan Meng
    Yang Xu
    Science China Information Sciences, 2013, 56 : 1 - 12
  • [4] α-GROUP LOCK RESOLUTION PRINCIPLE BASED ON LATTICE-VALUED PROPOSITIONAL LOGIC LP(X)
    Zhu, Hua
    Xu, Yang
    Zhao, Jianbin
    DECISION MAKING AND SOFT COMPUTING, 2014, 9 : 382 - 387
  • [5] α-LOCK SEMANTIC RESOLUTION METHOD BASED ON LATTICE-VALUED PROPOSITIONAL LOGIC LP(X)
    Zhong, Xiaomei
    Xu, Yang
    Chen, Shangyun
    He, Xingxing
    UNCERTAINTY MODELLING IN KNOWLEDGE ENGINEERING AND DECISION MAKING, 2016, 10 : 471 - 476
  • [6] On Compactness and Consistency in Finite Lattice-Valued Propositional Logic
    Pan, Xiaodong
    Xu, Yang
    Martinez, Luis
    Ruan, Da
    Liu, Jun
    HYBRID ARTIFICIAL INTELLIGENCE SYSTEMS, PT 2, 2010, 6077 : 328 - +
  • [7] Semantic theory of finite lattice-valued propositional logic
    XiaoDong Pan
    Yang Xu
    Science China Information Sciences, 2010, 53 : 2022 - 2031
  • [8] Semantic theory of finite lattice-valued propositional logic
    PAN XiaoDong 1
    2 Intelligent Control Development Center
    Science China(Information Sciences), 2010, 53 (10) : 2022 - 2031
  • [9] Syntax theory of finite lattice-valued propositional logic
    PAN XiaoDong
    MENG Dan
    XU Yang
    ScienceChina(InformationSciences), 2013, 56 (08) : 177 - 188
  • [10] Semantic theory of finite lattice-valued propositional logic
    Pan XiaoDong
    Xu Yang
    SCIENCE CHINA-INFORMATION SCIENCES, 2010, 53 (10) : 2022 - 2031
12345