A resolution procedure based on a fuzzy logic
Liu Jun, Song Zhenming, Qin Keyun · 2002
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/sub /spl aleph//. So we firstly focus on the resolution principle for Lukasiewicz logic L/sub /spl aleph//. 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/sub /spl aleph// are given. Moreover, a resolution-like rule, i.e., MP rule is proposed. By use of the MP rule, a resolution procedure in L/sub /spl aleph// 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.