Resolution principle based on six lattice-valued proposition logic LP/sub 6/(X)

Resolution-based automated reasoning theory is an important and active research field in artificial intelligence. It is used to judge the satisfiability of any logic formula. With the development of classical and non-classical logic, the resolution theory and method based on different logic system has been discussed widely and deeply. In the present paper, a new resolution principle by using ultrafilter in LP/sub 6/(X) is put forward. Different from existed method of resolution, this resolution in this paper is based on ultrafilter of lattice implication algebra. Because of LP/sub 6/(X) is a non-chain, non-boolean and non-well-ordered algebra structure, resolution based on LP/sub 6/(X) can be the theoretical foundation of resolution on lattice-valued truth-field. Accordingly, the research in this paper is helpful supported for the application of intelligent reasoning system based on lattice-valued logic.