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. The paper aims at the resolution principle for the Pavelka type fuzzy logic. 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 short L_ℵ. So we firstly focus on the resolution principle for Lukasiewicz logic L_ℵ. Some limitations of classical resolution and resolution procedures for some fuzzy logics are analyzed. Then some preliminary ideals about combining resolution procedure with the implication connectives in L_ℵ are given. Moreover, a resolution-like rule, i.e., MP rule is proposed. By use of the MP rule, a resolution procedure in L_ℵ is proposed and the soundness theorem of this resolution procedure is also proved. Finally, we apply the resolution to a Horn clause with truth-value in an enriched residuated lattice as Pavelka (1979) discussed