# zbMATH — the first resource for mathematics

Filter-based resolution principle for lattice-valued propositional logic LP$$(X)$$. (English) Zbl 1114.03019
Summary: As one of the most powerful approaches in automated reasoning, the resolution principle has been introduced to nonclassical logics, such as many-valued logic. However, most of the existing works are limited to the chain-type truth-value fields. Lattice-valued logics are a kind of important nonclassical logics, 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 a lattice implication algebra is presented, where the 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 first. 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 theorem for the presented approach are proved.

##### MSC:
 03B52 Fuzzy logic; logic of vagueness 03B35 Mechanization of proofs and logical operations
##### Software:
DISCOUNT; OTTER; CLIN
Full Text: