alpha-Resolution Method for Lattice-Valued Horn Generalized Clauses in Lattice-Valued First-Order Logic System

This paper presents an α-resolution method for lattice-valued Horn generalized clauses in lattice-valued first-order logic system LF(X) based on lattice implication algebra. In LF(X), we give the concepts of lattice-valued Horn generalized clause and normal lattice-valued Horn generalized clause. The α-resolvent of two lattice-valued Horn generalized clauses is also represented in LF(X). By using a substitution in each resolution process, we delete α-resolution literals and obtain their resolvent. At the same time, completeness theorems are also established. The present method can provide an efficient tool for automated reasoning in lattice-valued first-order logic system.