We continue the formal development of rough inclusion functions (RIFs), continuing the research on the formalization of rough sets  – 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 Gomolińska . We expand this framework introducing Jaccard index, Steinhaus generate metric, and Marczewski-Steinhaus metric space . This is the continuation of ; additionally we implement also parts of , , and the details of this work can be found in .
The subset sum problem is a basic problem in the field of theoretical computer science, especially in the complexity theory . The input is a sequence of positive integers and a target positive integer. The task is to determine if there exists a subsequence of the input sequence with sum equal to the target integer. It is known that the problem is NP-hard  and can be solved by dynamic programming in pseudo-polynomial time . In this article we formalize the recurrence relation of the dynamic programming.
In this paper we demonstrate the feasibility of formalizing recreational mathematics in Mizar (, ) drawing examples from W. Sierpinski’s book “250 Problems in Elementary Number Theory” . 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.
Timothy Makarios (with Isabelle/HOL1) and John Harrison (with HOL-Light2) shown that “the Klein-Beltrami model of the hyperbolic plane satisfy all of Tarski’s axioms except his Euclidean axiom” ,,,.
With the Mizar system  we use some ideas taken from Tim Makarios’s MSc thesis  to formalize some definitions (like the absolute) and lemmas necessary for the verification of the independence of the parallel postulate. In this article we prove that our constructed model (we prefer “Beltrami-Klein” name over “Klein-Beltrami”, which can be seen in the naming convention for Mizar functors, and even MML identifiers) satisfies the congruence symmetry, the congruence equivalence relation, and the congruence identity axioms formulated by Tarski (and formalized in Mizar as described briefly in ).
Timothy Makarios (with Isabelle/HOL1) and John Harrison (with HOL-Light2) shown that “the Klein-Beltrami model of the hyperbolic plane satisfy all of Tarski’s axioms except his Euclidean axiom” ,,[4, 5].
With the Mizar system  we use some ideas taken from Tim Makarios’s MSc thesis  to formalize some definitions and lemmas necessary for the verification of the independence of the parallel postulate. In this article, which is the continuation of , we prove that our constructed model satisfies the axioms of segment construction, the axiom of betweenness identity, and the axiom of Pasch due to Tarski, as formalized in  and related Mizar articles.
This article contains many auxiliary theorems which were missing in the Mizar Mathematical Library  to the best of the author’s knowledge. Most of them regard graph theory as formalized in the GLIB series (cf. ) and most of them are preliminaries needed in  or other forthcoming articles.
We continue in the Mizar system  the formalization of fuzzy implications according to the book of Baczyński and Jayaram “Fuzzy Implications” . In this article we define fuzzy negations and show their connections with previously defined fuzzy implications  and  and triangular norms and conorms . This can be seen as a step towards building a formal framework of fuzzy connectives . 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 ,  in Mizar  started in  and partially described in . 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 .
In the Mizar system (, ), Józef Białas has already given the one-dimensional Lebesgue measure . 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 , .