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

DOI

10.1080/18756891.2015.1129580How to use a DOI?

Keywords

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

Abstract

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.

Copyright

© 2017, the Authors. Published by Atlantis Press.

Open Access

This is an open access article distributed under the CC BY-NC license (http://creativecommons.org/licenses/by-nc/4.0/).

Download article (PDF)

TY  - JOUR
AU  - Weitao Xu
AU  - Wenqiang Zhang
AU  - Dexian Zhang
AU  - Yang Xu
AU  - Xiaodong Pan
PY  - 2015
DA  - 2015/12/01
TI  - α-Resolution Method for Lattice-valued Horn Generalized Clauses in Lattice-valued Propositional Logic Systems
JO  - International Journal of Computational Intelligence Systems
SP  - 75
EP  - 84
VL  - 8
IS  - Supplement 1
SN  - 1875-6883
UR  - https://doi.org/10.1080/18756891.2015.1129580
DO  - 10.1080/18756891.2015.1129580
ID  - Xu2015
ER  -