α-Resolution Method for Lattice-valued Horn Generalized Clauses in Lattice-valued Propositional Logic Systems

Abstract

In this paper, an α-resolution method for a set of lattice-valued Horn generalized clauses is established in lattice-valued propositional logic system L 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 L P(X ). Then, the α-resolution of two lattice-valued Horn generalized clauses is represented in L 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 L 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.

Keywords:

• automated reasoning
• lattice-valued logic
• α-resolution
• lattice-valued Horn g-clause
• lattice implication algebra