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; Jan Wagemans

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, Jan Wagemans

Research output › peer-review

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 theAlpha-satisability 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 verication procedure in the semantic level. Then, an alpha-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 e±cient resolution based automated reasoning in LP(X).

Original language	English
Title of host publication	Hybrid Artificial Intelligence Systems
Place of Publication	Heidelberg, Germany
Pages	320-327
Volume	2
State	Published - Jun 2010
Event	Hybrid Artificial Intelligence Systems - 5th International Conference HAIS2010, San Sebastián Duration: 23 Jun 2010 → 25 Jun 2010

Publication series

Name	Lecture Notes in Artificial Intelligence
Number	6077

Conference

Conference	Hybrid Artificial Intelligence Systems
Country/Territory	Spain
City	San Sebastián
Period	2010-06-23 → 2010-06-25

Cite this

@inproceedings{bd9d63b5fe734f59ad71ff68f6933cee,

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 theAlpha-satisability 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 verication procedure in the semantic level. Then, an alpha-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 e±cient resolution based automated reasoning in LP(X).",

keywords = "lattice-valued logic, Alpha-resolution principle, Alpha-satisability, ALpha-lock resolution method",

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

note = "Score = 3; Hybrid Artificial Intelligence Systems ; Conference date: 23-06-2010 Through 25-06-2010",

year = "2010",

month = jun,

language = "English",

isbn = "978-3-642-13802-7",

volume = "2",

series = "Lecture Notes in Artificial Intelligence",

number = "6077",

pages = "320--327",

booktitle = "Hybrid Artificial Intelligence Systems",

}

TY - GEN

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

A2 - Wagemans, Jan

N1 - Score = 3

PY - 2010/6

Y1 - 2010/6

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 theAlpha-satisability 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 verication procedure in the semantic level. Then, an alpha-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 e±cient 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 theAlpha-satisability 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 verication procedure in the semantic level. Then, an alpha-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 e±cient resolution based automated reasoning in LP(X).

KW - lattice-valued logic

KW - Alpha-resolution principle

KW - Alpha-satisability

KW - ALpha-lock resolution method

UR - http://ecm.sckcen.be/OTCS/llisapi.dll/open/ezp_111341

UR - http://ecm.sckcen.be/OTCS/llisapi.dll/open/ezp_111341_2

UR - http://knowledgecentre.sckcen.be/so2/bibref/7764

M3 - In-proceedings paper

SN - 978-3-642-13802-7

VL - 2

T3 - Lecture Notes in Artificial Intelligence

SP - 320

EP - 327

BT - Hybrid Artificial Intelligence Systems

CY - Heidelberg, Germany

T2 - Hybrid Artificial Intelligence Systems

Y2 - 23 June 2010 through 25 June 2010

ER -