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

• Main Authors: Weitao Xu, Wenqiang Zhang, Dexian Zhang, Yang Xu, Xiaodong Pan
• Format: Article
• Language: English
• Published: Atlantis Press 2015-12-01
• Series: International Journal of Computational Intelligence Systems
• Subjects: automated reasoning; lattice-valued logic; α-resolution; lattice-valued Horn g-clause; lattice implication algebra
• Online Access: https://www.atlantis-press.com/article/25868666.pdf

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.