A resolution procedure based on a fuzzy logic

As the use of non-classical logics become increasingly important in computer science, artificial intelligence and logic programming, the development of efficient automated theorem proving based on non-classical logic is currently an active area of research. This paper aims at the resolution principle for the Pavelka type fuzzy logic ([16]). Pavelka had shown in 1979 that the only natural way of formalizing fuzzy logic for truth values in the unit interval [0, 1] is by using Lukasiewicz's implication operator, in shortly L-N. So we firstly focus on the resolution principle for Lukasiewicz logic L-N. Some limitations of classical resolution and resolution procedures for some fuzzy logic are analyzed. Then some preliminary ideals about combining resolution procedure with the implication connectives in L-N are given. Moreover, a resolution-like rule, i.e., MP rule is proposed. By using of the MP rule, a resolution procedure in L-N was proposed and the soundness theorem of this resolution procedure was also proved. Finally, we use the resolution to Horn clause with truth-value in an enriched residuated lattice as Pavelka discussed.