Resolution principle based on six lattice-valued first-order logic L6F(X)

Resolution-based automated reasoning theory is an important and active research field in artificial intelligence. It is not only used to judge the satisfiability of any logic formula, but also widely applied to areas such as artificial intelligence, logic programming, problem solving and question answering systems, database theory, and so on. With the development of classical and non-classical logic, resolution theory and method based on different logic system has been discussed widely and deeply. In the present paper, resolution-based automated reasoning theory in a six lattice-valued first-order logic is focused. This resolution principle in this paper is based on ultrafilter of lattice implication algebra. In this paper, some necessary preliminaries are given first. Then resolution principle in L₆F(X) is discussed and soundness and completeness theorem is proved. Because of L₆F(X) is a non-chain, non-boolean and non-well-ordered algebra structure, resolution based on L₆F(X) is the theoretical foundation of resolution on lattice-valued truth-field. Accordingly, the research in this paper is a helpful support for the application of intelligent reasoning system based on lattice-valued logic which includes incomparable information.