A Sound and Complete Fuzzy Logic System Using Zadeh's Implication Operator
Sukhanu Kundu · 1995
We present a formalization of fuzzy logic based on Zadeh's implication operator a---~b = max{1-a, b}. Our logical system allows the specification of both lower and upper bounds of the truth value of a formula. We present a specific system of axioms and inference rules which are both sound and complete. We also provide a gener- alization of the classical resolution method which acts as a decision procedure in a finite fuzzy theory. We consider fuzzy propositional logic with t~uth values in the interval (0, 1). This work is motivated by Pavelka's formalization (10) of fuzzy logic based on Lukasiewicz's impIica- tion. In (10), the logical system allows one to infer the lower-bound for the troth value of a for- mula. In (5), a formalization of fuzzy logic using Zadeh's implication was presented, which allows one to infer the upper-bound of a formula. Although several sound inference rules were identified here, they were not complete in that they may not always allow us to infer the best possible upper-bound. In this paper, we combine the ideas in (5) and (10) to define the notions of both the lower and the upper bounds for semantic truth of a formula from a given fuzzy the- ory. We then propose a particular axiom system and inference rules based on Zadeh's implica- tion, and prove the soundness and completeness of the inference rules. We also present a fuzzy-resolution proof procedure which terminates for any finite fuzzy theory. Our axiom sys- tem is simpler than the one in (10), due to the fact that the formulas that we consider are sim- pier. For instance, in our case a formula like (A ~ 0.3) has truth value 0 or 1, whereas in (10)