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

Xingxing He; Jun Liu; Yang Xu; Luis Martínez; Da Ruan

doi:10.1093/jigpal/jzr007

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

Xingxing He
, Jun Liu
, Yang Xu
, Luis Martínez
, Da Ruan

Research output › peer-review

Abstract

Automated reasoning issues are addressed for a finite lattice-valued propositional logic L_nP(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 L_nP(X) to simplify the procedure in the semantic level for testing the satisfiability of formulas in L_nP(X) at a certain truth-value level α (α-satisfiability) while keeping the role of truth constant formula played in L_nP(X). We propose a lock resolution method at a certain truth-value level α (α-lock resolution) in L_nP(X) and have proved its theorems of soundness and weak completeness, respectively. We provide more efficient resolution based automated reasoning in L_nP(X) and key supports for α-resolution-based automated reasoning approaches and algorithms in lattice based linguistic truth-valued logic.

Original language	English
Pages (from-to)	579-588
Number of pages	10
Journal	Logic Journal of the IGPL
Volume	20
Issue number	3
DOIs	https://doi.org/10.1093/jigpal/jzr007
State	Published - Jun 2012

ASJC Scopus subject areas

Logic

Access to Document

10.1093/jigpal/jzr007License: Unspecified

Cite this

@article{5ba5978592b6424392ecd8ee388597c5,

title = "On α-satisfiability and its α-lock resolution in a finite lattice-valued propositional logic",

abstract = "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 α (α-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 α (α-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 α-resolution-based automated reasoning approaches and algorithms in lattice based linguistic truth-valued logic.",

keywords = "Finite lattice-valued propositional logic, Lattice-valued logic, α-lock resolution method, α-resolution principle, α-satisfiability",

author = "Xingxing He and Jun Liu and Yang Xu and Luis Mart{\'i}nez and Da Ruan",

year = "2012",

month = jun,

doi = "10.1093/jigpal/jzr007",

language = "English",

volume = "20",

pages = "579--588",

journal = "Logic Journal of the IGPL",

issn = "1367-0751",

publisher = "Oxford University Press",

number = "3",

}

TY - JOUR

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

AU - He, Xingxing

AU - Liu, Jun

AU - Xu, Yang

AU - Martínez, Luis

AU - Ruan, Da

PY - 2012/6

Y1 - 2012/6

N2 - 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 α (α-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 α (α-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 α-resolution-based automated reasoning approaches and algorithms in lattice based linguistic truth-valued logic.

AB - 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 α (α-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 α (α-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 α-resolution-based automated reasoning approaches and algorithms in lattice based linguistic truth-valued logic.

KW - Finite lattice-valued propositional logic

KW - Lattice-valued logic

KW - α-lock resolution method

KW - α-resolution principle

KW - α-satisfiability

UR - https://www.scopus.com/pages/publications/84861812629

U2 - 10.1093/jigpal/jzr007

DO - 10.1093/jigpal/jzr007

M3 - Article

AN - SCOPUS:84861812629

SN - 1367-0751

VL - 20

SP - 579

EP - 588

JO - Logic Journal of the IGPL

JF - Logic Journal of the IGPL

IS - 3

ER -