Computer-Supported Encoding of Fuzzy Negations and Laws of Contraposition

This work is the continuation of a research towards preparing formal counterpart of the fuzzy implications and corresponding issues according to the textbook by Baczyński and Jarayam “Fuzzy Implications”. Here, using the Mizar system and the Mizar Mathematical Library we build the bridge of notions needed to study the laws of contraposition for fuzzy implications (Sect. 1.5) and in order to do that, we also had to cope with generation of fuzzy negations from fuzzy implications. Similarly as earlier in the case of implications and t-norms/conorms, although it is quite uncommon for Mizar, we build a bunch of useful examples corresponding to these specific fuzzy connectives, just to test the efficiency of the formal apparatus; in the same time we obtain the net of registrations of clusters allowing for automatic type generation for corresponding objects.