http://hdl.handle.net/11320/12384 2026-06-01T20:21:38Z http://hdl.handle.net/11320/12393 Tytuł: Some Properties of Membership Functions Composed of Triangle Functions and Piecewise Linear Functions Autorzy: Mitsuishi, Takashi Abstrakt: IF-THEN rules in fuzzy inference is composed of multiple fuzzy sets (membership functions). IF-THEN rules can therefore be considered as a pair of membership functions [7]. The evaluation function of fuzzy control is composite function with fuzzy approximate reasoning and is functional on the set of membership functions. We obtained continuity of the evaluation function and compactness of the set of membership functions [12]. Therefore, we proved the existence of pair of membership functions, which maximizes (minimizes) evaluation function and is considered IF-THEN rules, in the set of membership functions by using extreme value theorem. The set of membership functions (fuzzy sets) is defined in this article to verifier our proofs before by Mizar [9], [10], [4]. Membership functions composed of triangle function, piecewise linear function and Gaussian function used in practice are formalized using existing functions. On the other hand, not only curve membership functions mentioned above but also membership functions composed of straight lines (piecewise linear function) like triangular and trapezoidal functions are formalized. Moreover, different from the definition in [3] formalizations of triangular and trapezoidal function composed of two straight lines, minimum function and maximum functions are proposed. We prove, using the Mizar [2], [1] formalism, some properties of membership functions such as continuity and periodicity [13], [8]. 2021-01-01T00:00:00Z http://hdl.handle.net/11320/12392 Tytuł: On Primary Ideals. Part I Autorzy: Watase, Yasushige Abstrakt: We formalize in the Mizar System [3], [4], definitions and basic propositions about primary ideals of a commutative ring along with Chapter 4 of [1] and Chapter III of [8]. Additionally other necessary basic ideal operations such as compatibilities taking radical and intersection of finite number of ideals are formalized as well in order to prove theorems relating primary ideals. These basic operations are mainly quoted from Chapter 1 of [1] and compiled as preliminaries in the first half of the article. 2021-01-01T00:00:00Z http://hdl.handle.net/11320/12390 Tytuł: Ascoli-Arzelà Theorem Autorzy: Yamazaki, Hiroshi; Miyajima, Keiichi; Shidama, Yasunari Abstrakt: In this article we formalize the Ascoli-Arzelà theorem [5], [6], [8] in Mizar [1], [2]. First, we gave definitions of equicontinuousness and equiboundedness of a set of continuous functions [12], [7], [3], [9]. Next, we formalized the Ascoli-Arzelà theorem using those definitions, and proved this theorem. 2021-01-01T00:00:00Z http://hdl.handle.net/11320/12387 Tytuł: On Weakly Associative Lattices and Near Lattices Autorzy: Sawicki, Damian; Grabowski, Adam Abstrakt: The main aim of this article is to introduce formally two generalizations of lattices, namely weakly associative lattices and near lattices, which can be obtained from the former by certain weakening of the usual well-known axioms. We show selected propositions devoted to weakly associative lattices and near lattices from Chapter 6 of [15], dealing also with alternative versions of classical axiomatizations. Some of the results were proven in the Mizar [1], [2] system with the help of Prover9 [14] proof assistant. 2021-01-01T00:00:00Z