α - Lock resolution method for a lattice-valued first-order logic

Xingxing He; Yang Xu; Jun Liu; Da Ruan

doi:10.1016/j.engappai.2011.07.003

α - Lock resolution method for a lattice-valued first-order logic

Xingxing He, Yang Xu, Jun Liu, Da Ruan

Research output › peer-review

Abstract

This paper focuses on resolution-based automated reasoning approaches in a lattice-valued first-order logic LF(X) with truth-values defined in a logical algebraic structure - lattice implication algebra (LIA), which aims at providing the logic foundation to represent and handle both imprecision and incomparability. In order to improve the efficiency of α-resolution approach proposed for LF(X), firstly the concepts of α-lock resolution principle and deduction are introduced for lattice-valued propositional logic LP(X) based on LIA, along with its soundness and weak completeness theorems. Then all the results are extended into LF(X) by using Lifting Lemma. Finally an α-lock resolution automated reasoning algorithm in LF(X) is proposed for the implementation purpose. This work provides a theoretical foundation for more efficient resolution-based automated reasoning algorithm in lattice-valued logic LF(X).

Original language	English
Pages (from-to)	1274-1280
Number of pages	7
Journal	Engineering Applications of Artificial Intelligence
Volume	24
Issue number	7
DOIs	https://doi.org/10.1016/j.engappai.2011.07.003
State	Published - Oct 2011

ASJC Scopus subject areas

Control and Systems Engineering
Artificial Intelligence
Electrical and Electronic Engineering

Access to Document

10.1016/j.engappai.2011.07.003License: Unspecified

Cite this

@article{659dced501af4c69b85371d63233727c,

title = "α - Lock resolution method for a lattice-valued first-order logic",

abstract = "This paper focuses on resolution-based automated reasoning approaches in a lattice-valued first-order logic LF(X) with truth-values defined in a logical algebraic structure - lattice implication algebra (LIA), which aims at providing the logic foundation to represent and handle both imprecision and incomparability. In order to improve the efficiency of α-resolution approach proposed for LF(X), firstly the concepts of α-lock resolution principle and deduction are introduced for lattice-valued propositional logic LP(X) based on LIA, along with its soundness and weak completeness theorems. Then all the results are extended into LF(X) by using Lifting Lemma. Finally an α-lock resolution automated reasoning algorithm in LF(X) is proposed for the implementation purpose. This work provides a theoretical foundation for more efficient resolution-based automated reasoning algorithm in lattice-valued logic LF(X).",

keywords = "α - Lock resolution, α - Resolution, Automated reasoning, Lattice implication algebra, Lattice-valued logic",

author = "Xingxing He and Yang Xu and Jun Liu and Da Ruan",

year = "2011",

month = oct,

doi = "10.1016/j.engappai.2011.07.003",

language = "English",

volume = "24",

pages = "1274--1280",

journal = "Engineering Applications of Artificial Intelligence",

issn = "0952-1976",

publisher = "Elsevier B.V.",

number = "7",

}

TY - JOUR

T1 - α - Lock resolution method for a lattice-valued first-order logic

AU - He, Xingxing

AU - Xu, Yang

AU - Liu, Jun

AU - Ruan, Da

PY - 2011/10

Y1 - 2011/10

N2 - This paper focuses on resolution-based automated reasoning approaches in a lattice-valued first-order logic LF(X) with truth-values defined in a logical algebraic structure - lattice implication algebra (LIA), which aims at providing the logic foundation to represent and handle both imprecision and incomparability. In order to improve the efficiency of α-resolution approach proposed for LF(X), firstly the concepts of α-lock resolution principle and deduction are introduced for lattice-valued propositional logic LP(X) based on LIA, along with its soundness and weak completeness theorems. Then all the results are extended into LF(X) by using Lifting Lemma. Finally an α-lock resolution automated reasoning algorithm in LF(X) is proposed for the implementation purpose. This work provides a theoretical foundation for more efficient resolution-based automated reasoning algorithm in lattice-valued logic LF(X).

AB - This paper focuses on resolution-based automated reasoning approaches in a lattice-valued first-order logic LF(X) with truth-values defined in a logical algebraic structure - lattice implication algebra (LIA), which aims at providing the logic foundation to represent and handle both imprecision and incomparability. In order to improve the efficiency of α-resolution approach proposed for LF(X), firstly the concepts of α-lock resolution principle and deduction are introduced for lattice-valued propositional logic LP(X) based on LIA, along with its soundness and weak completeness theorems. Then all the results are extended into LF(X) by using Lifting Lemma. Finally an α-lock resolution automated reasoning algorithm in LF(X) is proposed for the implementation purpose. This work provides a theoretical foundation for more efficient resolution-based automated reasoning algorithm in lattice-valued logic LF(X).

KW - α - Lock resolution

KW - α - Resolution

KW - Automated reasoning

KW - Lattice implication algebra

KW - Lattice-valued logic

UR - http://www.scopus.com/inward/record.url?scp=80052264269&partnerID=8YFLogxK

U2 - 10.1016/j.engappai.2011.07.003

DO - 10.1016/j.engappai.2011.07.003

M3 - Article

AN - SCOPUS:80052264269

SN - 0952-1976

VL - 24

SP - 1274

EP - 1280

JO - Engineering Applications of Artificial Intelligence

JF - Engineering Applications of Artificial Intelligence

IS - 7

ER -