Determination of α-resolution in lattice-valued first-order logic LF(X)

Yang Xu; Jun Liu; Da Ruan; Xiaobing Li

doi:10.1016/j.ins.2010.03.024

Determination of α-resolution in lattice-valued first-order logic LF(X)

Yang Xu, Jun Liu, Da Ruan, Xiaobing Li

Research output › peer-review

Abstract

Key issues for resolution-based automated reasoning in lattice-valued first-order logic LF(X) are investigated with truth-values in a lattice-valued logical algebraic structure–lattice implication algebra (LIA). The determination of resolution at a certain truth-value level (called α-resolution) in LF(X) is proved to be equivalently transformed into the determination of α-resolution in lattice-valued propositional logic LP(X) based on LIA. The determination of α-resolution of any quasi-regular generalized literals and constants under various cases in LP(X) is further analyzed, specified, and subsequently verified. Hence the determination of α-resolution in LF(X) can be accordingly solved to a very broad extent, which not only lays a foundation for the practical implementation of automated reasoning algorithms in LF(X), but also provides a key support for α-resolution-based automated reasoning approaches and algorithms in LIA based linguistic truth-valued logics.

Original language	English
Pages (from-to)	1836-1862
Number of pages	27
Journal	Information Sciences
Volume	181
Issue number	10
DOIs	https://doi.org/10.1016/j.ins.2010.03.024
State	Published - 15 May 2011

Access to Document

10.1016/j.ins.2010.03.024License: Unspecified

Cite this

@article{0d3d7dbb186f4b719041ecc858cf3769,

title = "Determination of α-resolution in lattice-valued first-order logic LF(X)",

abstract = "Key issues for resolution-based automated reasoning in lattice-valued first-order logic LF(X) are investigated with truth-values in a lattice-valued logical algebraic structure–lattice implication algebra (LIA). The determination of resolution at a certain truth-value level (called α-resolution) in LF(X) is proved to be equivalently transformed into the determination of α-resolution in lattice-valued propositional logic LP(X) based on LIA. The determination of α-resolution of any quasi-regular generalized literals and constants under various cases in LP(X) is further analyzed, specified, and subsequently verified. Hence the determination of α-resolution in LF(X) can be accordingly solved to a very broad extent, which not only lays a foundation for the practical implementation of automated reasoning algorithms in LF(X), but also provides a key support for α-resolution-based automated reasoning approaches and algorithms in LIA based linguistic truth-valued logics.",

keywords = "Incomparability, Many-valued logic, Automated reasoning, Lattice implication algebra, Lattice-valued logic, α-Resolution",

author = "Yang Xu and Jun Liu and Da Ruan and Xiaobing Li",

note = "Score=10",

year = "2011",

month = may,

day = "15",

doi = "10.1016/j.ins.2010.03.024",

language = "English",

volume = "181",

pages = "1836--1862",

journal = "Information Sciences",

issn = "0020-0255",

publisher = "Elsevier Inc.",

number = "10",

}

TY - JOUR

T1 - Determination of α-resolution in lattice-valued first-order logic LF(X)

AU - Xu, Yang

AU - Liu, Jun

AU - Ruan, Da

AU - Li, Xiaobing

N1 - Score=10

PY - 2011/5/15

Y1 - 2011/5/15

N2 - Key issues for resolution-based automated reasoning in lattice-valued first-order logic LF(X) are investigated with truth-values in a lattice-valued logical algebraic structure–lattice implication algebra (LIA). The determination of resolution at a certain truth-value level (called α-resolution) in LF(X) is proved to be equivalently transformed into the determination of α-resolution in lattice-valued propositional logic LP(X) based on LIA. The determination of α-resolution of any quasi-regular generalized literals and constants under various cases in LP(X) is further analyzed, specified, and subsequently verified. Hence the determination of α-resolution in LF(X) can be accordingly solved to a very broad extent, which not only lays a foundation for the practical implementation of automated reasoning algorithms in LF(X), but also provides a key support for α-resolution-based automated reasoning approaches and algorithms in LIA based linguistic truth-valued logics.

AB - Key issues for resolution-based automated reasoning in lattice-valued first-order logic LF(X) are investigated with truth-values in a lattice-valued logical algebraic structure–lattice implication algebra (LIA). The determination of resolution at a certain truth-value level (called α-resolution) in LF(X) is proved to be equivalently transformed into the determination of α-resolution in lattice-valued propositional logic LP(X) based on LIA. The determination of α-resolution of any quasi-regular generalized literals and constants under various cases in LP(X) is further analyzed, specified, and subsequently verified. Hence the determination of α-resolution in LF(X) can be accordingly solved to a very broad extent, which not only lays a foundation for the practical implementation of automated reasoning algorithms in LF(X), but also provides a key support for α-resolution-based automated reasoning approaches and algorithms in LIA based linguistic truth-valued logics.

KW - Incomparability

KW - Many-valued logic

KW - Automated reasoning

KW - Lattice implication algebra

KW - Lattice-valued logic

KW - α-Resolution

UR - https://ecm.sckcen.be/OTCS/llisapi.dll/overview/39155443

U2 - 10.1016/j.ins.2010.03.024

DO - 10.1016/j.ins.2010.03.024

M3 - Article

SN - 0020-0255

VL - 181

SP - 1836

EP - 1862

JO - Information Sciences

JF - Information Sciences

IS - 10

ER -