http://hdl.handle.net/11320/14263 2026-03-16T17:30:27Z 2026-03-16T17:30:27Z Korniłowicz, Artur http://hdl.handle.net/11320/14268 2022-12-30T12:04:05Z 2022-01-01T00:00:00Z

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.

2022-01-01T00:00:00Z Mitsuishi, Takashi http://hdl.handle.net/11320/14267 2022-12-30T11:26:35Z 2022-01-01T00:00:00Z

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.

2022-01-01T00:00:00Z Koch, Sebastian http://hdl.handle.net/11320/14266 2022-12-30T11:14:29Z 2022-01-01T00:00:00Z

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].

2022-01-01T00:00:00Z Nakasho, Kazuhisa http://hdl.handle.net/11320/14265 2022-12-30T11:06:13Z 2022-01-01T00:00:00Z

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.

2022-01-01T00:00:00Z