A resolution-like strategy based on a lattice-valued logic

As the use of nonclassical logics becomes increasingly important in computer science, artificial intelligence and logic programming, the development of efficient automated theorem proving based on nonclassical logic is currently an active area of research. This paper aims at the resolution principle for the Pavelka type fuzzy logic (1979). Pavelka showed that the only natural way of formalizing fuzzy logic for truth-values in the unit interval [0, 1] is by using the Lukasiewicz´s implication operator a→b=min{1,1-a+b} or some isomorphic forms of it. Hence, we first focus on the resolution principle for the Lukasiewicz logic L_ℵ with [0, 1] as the truth-valued set. Some limitations of classical resolution and resolution procedures for fuzzy logic with Kleene implication are analyzed. Then some preliminary ideals about combining resolution procedure with the implication connectives in L_ℵ are given. Moreover, a resolution-like principle in L_ℵ is proposed and the soundness theorem of this resolution procedure is also proved. Second, we use this resolution-like principle to Horn clauses with truth-values in an enriched residuated lattice and consider the L-type fuzzy Prolog.