α-RESOLUTION METHOD FOR LATTICE-VALUED HORN GENERALIZED CLAUSES IN LATTICE-VALUED PROPOSITIONAL LOGIC SYSTEM

摘要

This paper presents an α-resolution method for lattice-valued horn generalized clauses in lattice-valued propositional logic system (£)P(X) based on lattice implication algebra. In this approach, We give lattice-valued horn generalized clause and the correlative concepts in (£)P(X). The α-resolution of two lattice-valued horn generalized clauses is also represented in (£)P(X). It reflects the resolution rules in a resolution process, which aims at deleting α-resolution literals and obtaining a resolvent. This method can provide an efficient tool for automated reasoning in lattice-valued propositional logic system and lattice-valued first-order logic system.