Alpha-satisfiability and alpha-lock resolution for a lattice-valued logic LP(X)

Xingxing He; Yang Xu; Yingfang Li; Jun Liu; Luis Martinez; Da Ruan

doi:10.1007/978-3-642-13803-4_40

Alpha-satisfiability and alpha-lock resolution for a lattice-valued logic LP(X)

Xingxing He, Yang Xu, Yingfang Li, Jun Liu, Luis Martinez, Da Ruan

Research output › peer-review

8 Scopus citations

Abstract

This paper focuses on some automated reasoning issues for a kind of lattice-valued logic LP(X) based on lattice-valued algebra. Firstly some extended strategies from classical logic to LP(X) are investigated in order to verify the α-satisfiability of formulae in LP(X) while the main focus is given on the role of constant formula played in LP(X) in order to simply the verification procedure in the semantic level. Then, an α-lock resolution method in LP(X) is proposed and the weak completeness of this method is proved. The work will provide a support for the more efficient resolution based automated reasoning in LP(X).

Original language	English
Pages (from-to)	320-327
Number of pages	8
Journal	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	6077 LNAI
Issue number	PART 2
DOIs	https://doi.org/10.1007/978-3-642-13803-4_40
State	Published - 2010
Event	HAIS - 2010: 5th International Conference on Hybrid Artificial Intelligence Systems - 5th International Conference HAIS2010, San Sebastian Duration: 23 Jun 2010 → 25 Jun 2010

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Access to Document

10.1007/978-3-642-13803-4_40

Cite this

@article{b46e117cda5f4ac6a797c970e4c28a5a,

title = "Alpha-satisfiability and alpha-lock resolution for a lattice-valued logic LP(X)",

abstract = "This paper focuses on some automated reasoning issues for a kind of lattice-valued logic LP(X) based on lattice-valued algebra. Firstly some extended strategies from classical logic to LP(X) are investigated in order to verify the α-satisfiability of formulae in LP(X) while the main focus is given on the role of constant formula played in LP(X) in order to simply the verification procedure in the semantic level. Then, an α-lock resolution method in LP(X) is proposed and the weak completeness of this method is proved. The work will provide a support for the more efficient resolution based automated reasoning in LP(X).",

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

author = "Xingxing He and Yang Xu and Yingfang Li and Jun Liu and Luis Martinez and Da Ruan",

year = "2010",

doi = "10.1007/978-3-642-13803-4_40",

language = "English",

volume = "6077 LNAI",

pages = "320--327",

journal = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

issn = "0302-9743",

publisher = "Springer Science and Business Media Deutschland GmbH",

number = "PART 2",

note = "HAIS - 2010 : 5th International Conference on Hybrid Artificial Intelligence Systems, HAIS ; Conference date: 23-06-2010 Through 25-06-2010",

}

TY - JOUR

T1 - Alpha-satisfiability and alpha-lock resolution for a lattice-valued logic LP(X)

AU - He, Xingxing

AU - Xu, Yang

AU - Li, Yingfang

AU - Liu, Jun

AU - Martinez, Luis

AU - Ruan, Da

PY - 2010

Y1 - 2010

N2 - This paper focuses on some automated reasoning issues for a kind of lattice-valued logic LP(X) based on lattice-valued algebra. Firstly some extended strategies from classical logic to LP(X) are investigated in order to verify the α-satisfiability of formulae in LP(X) while the main focus is given on the role of constant formula played in LP(X) in order to simply the verification procedure in the semantic level. Then, an α-lock resolution method in LP(X) is proposed and the weak completeness of this method is proved. The work will provide a support for the more efficient resolution based automated reasoning in LP(X).

AB - This paper focuses on some automated reasoning issues for a kind of lattice-valued logic LP(X) based on lattice-valued algebra. Firstly some extended strategies from classical logic to LP(X) are investigated in order to verify the α-satisfiability of formulae in LP(X) while the main focus is given on the role of constant formula played in LP(X) in order to simply the verification procedure in the semantic level. Then, an α-lock resolution method in LP(X) is proposed and the weak completeness of this method is proved. The work will provide a support for the more efficient resolution based automated reasoning in LP(X).

KW - α-lock resolution method

KW - α-resolution principle

KW - α-satisfiability

KW - Lattice-valued logic

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

U2 - 10.1007/978-3-642-13803-4_40

DO - 10.1007/978-3-642-13803-4_40

M3 - Article

AN - SCOPUS:77954616788

SN - 0302-9743

VL - 6077 LNAI

SP - 320

EP - 327

JO - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

JF - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

IS - PART 2

T2 - HAIS - 2010

Y2 - 23 June 2010 through 25 June 2010

ER -