Formalization and Verification of Fuzzy Approximate Reasoning by Mizar

In this paper, we describe the verification and formalization of fuzzy optimal control problems using the proof checker Mizar. First, we provide a brief introduction to fuzzy inference. In order to achieve the optimization of fuzzy optimal control, the compactness of the family of membership functions and two types of continuity of fuzzy approximate reasoning are required. We have proven the existence of IT-THEN rules that minimize the performance function for fuzzy control. To verify these properties using Mizar, we formalize the set of membership functions as a generalization of IT-THEN rules. Additionally, we verify the properties of piecewise linear functions. Furthermore, we formalize the definition of the defuzzified value using the centroid method in the Mizar language. The paper also explains several theorems and definitions concerning fuzzy logic, which are written in the Mizar language.