| Summary: | In this paper, an α-resolution method for a set of lattice-valued Horn generalized clauses is established in lattice-valued propositional logic system ℒ P(X) based on lattice implication algebra. Firstly, the notions of lattice-valued Horn generalized clause, normal lattice-valued Horn generalized clause and unit lattice-valued Horn generalized clause are given in ℒ P(X). Then, the α-resolution of two lattice-valued Horn generalized clauses is represented in ℒ P(X). It indicates the reasoning rules in a resolution process, which aims at deleting α-resolution literals and obtaining a resolvent. Finally, we build an α-resolution algorithm for a set of lattice-valued Horn generalized clauses in ℒ P(X). It provides a foundation for automated reasoning in lattice-valued first-order logic system and an application for designing an inference system in the field of intelligent decision support.
|
|---|
