http://hdl.handle.net/11320/9218 2026-06-01T15:15:41Z 2026-06-01T15:15:41Z Grabowski, Adam http://hdl.handle.net/11320/9229 2020-06-16T10:01:01Z 2020-01-01T00:00:00Z

Tytuł: On Fuzzy Negations Generated by Fuzzy Implications Autorzy: Grabowski, Adam Abstrakt: We continue in the Mizar system [2] the formalization of fuzzy implications according to the book of Baczynski and Jayaram “Fuzzy Implications” [1]. In this article we define fuzzy negations and show their connections with previously defined fuzzy implications [4] and [5] and triangular norms and conorms [6]. This can be seen as a step towards building a formal framework of fuzzy connectives [10]. We introduce formally Sugeno negation, boundary negations and show how these operators are pointwise ordered. This work is a continuation of the development of fuzzy sets [12], [3] in Mizar [7] started in [11] and partially described in [8]. This submission can be treated also as a part of a formal comparison of fuzzy and rough approaches to incomplete or uncertain information within the Mizar Mathematical Library [9].

2020-01-01T00:00:00Z Naumowicz, Adam http://hdl.handle.net/11320/9228 2020-06-16T08:30:15Z 2020-01-01T00:00:00Z

Tytuł: Elementary Number Theory Problems. Part I Autorzy: Naumowicz, Adam Abstrakt: In this paper we demonstrate the feasibility of formalizing recreational mathematics in Mizar ([1], [2]) drawing examples from W. Sierpinski’s book “250 Problems in Elementary Number Theory” [4]. The current work contains proofs of initial ten problems from the chapter devoted to the divisibility of numbers. Included are problems on several levels of difficulty.

2020-01-01T00:00:00Z Grabowski, Adam http://hdl.handle.net/11320/9227 2020-06-16T07:24:40Z 2020-01-01T00:00:00Z

Tytuł: Developing Complementary Rough Inclusion Functions Autorzy: Grabowski, Adam Abstrakt: We continue the formal development of rough inclusion functions (RIFs), continuing the research on the formalization of rough sets [15] – a well-known tool of modelling of incomplete or partially unknown information. In this article we give the formal characterization of complementary RIFs, following a paper by Gomolinska [4].We expand this framework introducing Jaccard index, Steinhaus generate metric, and Marczewski-Steinhaus metric space [1]. This is the continuation of [9]; additionally we implement also parts of [2], [3], and the details of this work can be found in [7].

2020-01-01T00:00:00Z Endou, Noboru http://hdl.handle.net/11320/9226 2020-06-16T07:25:16Z 2020-01-01T00:00:00Z

Tytuł: Reconstruction of the One-Dimensional Lebesgue Measure Autorzy: Endou, Noboru Abstrakt: In the Mizar system ([1], [2]), Józef Białas has already given the one-dimensional Lebesgue measure [4]. However, the measure introduced by Białas limited the outer measure to a field with finite additivity. So, although it satisfies the nature of the measure, it cannot specify the length of measurable sets and also it cannot determine what kind of set is a measurable set. From the above, the authors first determined the length of the interval by the outer measure. Specifically, we used the compactness of the real space. Next, we constructed the pre-measure by limiting the outer measure to a semialgebra of intervals. Furthermore, by repeating the extension of the previous measure, we reconstructed the one-dimensional Lebesgue measure [7], [3].

2020-01-01T00:00:00Z