http://hdl.handle.net/11320/14263 Mon, 09 Mar 2026 08:21:55 GMT 2026-03-09T08:21:55Z http://hdl.handle.net/11320/14268 Tytuł: Elementary Number Theory Problems. Part III Autorzy: Korniłowicz, Artur Abstrakt: In this paper problems 11, 16, 19–24, 39, 44, 46, 74, 75, 77, 82, and 176 from [10] are formalized as described in [6], using the Mizar formalism [1], [2], [4]. Problems 11 and 16 from the book are formulated as several independent theorems. Problem 46 is formulated with a given example of required properties. Problem 77 is not formulated using triangles as in the book is. Sat, 01 Jan 2022 00:00:00 GMT http://hdl.handle.net/11320/14268 2022-01-01T00:00:00Z http://hdl.handle.net/11320/14267 Tytuł: Definition of Centroid Method as Defuzzification Autorzy: Mitsuishi, Takashi Abstrakt: In this study, using the Mizar system [1], [2], we reuse formalization efforts in fuzzy sets described in [5] and [6]. This time the centroid method which is one of the fuzzy inference processes is formulated [10]. It is the most popular of all defuzzied methods ([11], [13], [7]) – here, defuzzified crisp value is obtained from domain of membership function as weighted average [8]. Since the integral is used in centroid method, the integrability and bounded properties of membership functions are also mentioned to fill the formalization gaps present in the Mizar Mathematical Library, as in the case of another fuzzy operators [4]. In this paper, the properties of piecewise linear functions consisting of two straight lines are mainly described. Sat, 01 Jan 2022 00:00:00 GMT http://hdl.handle.net/11320/14267 2022-01-01T00:00:00Z http://hdl.handle.net/11320/14266 Tytuł: Introduction to Graph Colorings Autorzy: Koch, Sebastian Abstrakt: In this article vertex, edge and total colorings of graphs are formalized in the Mizar system [4] and [1], based on the formalization of graphs in [5]. Sat, 01 Jan 2022 00:00:00 GMT http://hdl.handle.net/11320/14266 2022-01-01T00:00:00Z http://hdl.handle.net/11320/14265 Tytuł: Transformation Tools for Real Linear Spaces Autorzy: Nakasho, Kazuhisa Abstrakt: This paper, using the Mizar system [1], [2], provides useful tools for working with real linear spaces and real normed spaces. These include the identification of a real number set with a one-dimensional real normed space, the relationships between real linear spaces and real Euclidean spaces, the transformation from a real linear space to a real vector space, and the properties of basis and dimensions of real linear spaces. We referred to [6], [10], [8], [9] in this formalization. Sat, 01 Jan 2022 00:00:00 GMT http://hdl.handle.net/11320/14265 2022-01-01T00:00:00Z