TY - JOUR

T1 - Filter-based resolution principle for lattice-valued propositional logic LP(X)

AU - Ma, Jun

AU - Li, Wenjiang

AU - Ruan, Da

AU - Xu, Yang

A2 - Laes, Erik

A2 - Carlé, Benny

N1 - Score = 10

PY - 2007/2

Y1 - 2007/2

N2 - As one of most powerful approaches in automated reasoning, resolution principle has been introduced to non-classical logics, such as many-valued logic. However, most of the existing works are limited to the chain-type truth-value fields. Lattice-valued logic is a kind of important non-classical logic, which can be applied to describe and handle incomparability by the incomparable elements in its truth-value field. In this paper, a filter-based resolution principle for the lattice-valued propositional logic LP(X) based on lattice implication algebra is presented, where filter of the truth-value field being a lattice implication algebra is taken as the criterion for measuring the satisfiability of a lattice-valued logical formula. The notions and properties of lattice implication algebra, filter of lattice implication algebra, and the lattice-valued propositional logic LP(X) are given firstly. The definitions and structures of two kinds of lattice-valued logical formulae, i.e., the simple generalized clauses and complex generalized clauses, are presented then. Finally, the filter-based resolution principle is given and after that the soundness theorem and weak completeness theorems for the presented approach are proved.

AB - As one of most powerful approaches in automated reasoning, resolution principle has been introduced to non-classical logics, such as many-valued logic. However, most of the existing works are limited to the chain-type truth-value fields. Lattice-valued logic is a kind of important non-classical logic, which can be applied to describe and handle incomparability by the incomparable elements in its truth-value field. In this paper, a filter-based resolution principle for the lattice-valued propositional logic LP(X) based on lattice implication algebra is presented, where filter of the truth-value field being a lattice implication algebra is taken as the criterion for measuring the satisfiability of a lattice-valued logical formula. The notions and properties of lattice implication algebra, filter of lattice implication algebra, and the lattice-valued propositional logic LP(X) are given firstly. The definitions and structures of two kinds of lattice-valued logical formulae, i.e., the simple generalized clauses and complex generalized clauses, are presented then. Finally, the filter-based resolution principle is given and after that the soundness theorem and weak completeness theorems for the presented approach are proved.

KW - Resolution principle

KW - Filter

KW - Lattice-valued logic

KW - Automated reasoning

KW - Simple generalized clause

KW - Complex generalized clause

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

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

U2 - 10.1016/j.ins.2006.07.027

DO - 10.1016/j.ins.2006.07.027

M3 - Article

SN - 0020-0255

VL - 177

SP - 1046

EP - 1062

JO - Information Sciences

JF - Information Sciences

IS - 4

ER -