This paper is a description of first steps towards providing the computer-supported formalization of a relatively recent textbook by Baczyński and Jarayam “Fuzzy Implications”. We present some of the issues connected with the use of Mizar-computerized proof assistant together with its extensive repository of mathematical texts checked for their logical correctness called the Mizar Mathematical Library, based on Zermelo-Fraenkel set theory and classical first order logic. As some building blocks towards fuzzy numbers were provided, we implemented some important tools needed for proper formalization work, as nine basic fuzzy implications, opening also possibility of smooth introducing virtually any operators of such kind. Together with triangular norms and conorms this development seems promising as the preliminary step towards fuzzy logic in the repository of Mizar texts.

The paper contains some remarks on building automated counterpart of a comparison of some generalized rough approximations of sets, where the classical indiscernibility relation is generalized to arbitrary binary relation. Our focus was on translating rationality postulates for such operators by means of the Mizar system – the software and the database which allows for expressing and checking mathematical knowledge for the logical correctness. The main objective was the formal (and machine-checked) proof of Theorem 4.1 from A. Gomolińska’s paper “A Comparative Study of Some Generalized Rough Approximations”, hence the present title. We provide also the discussion on how to make the presentation more efficient to reuse the reasoning techniques of the Mizar verifier.

The Mizar system is one of the pioneering systems aimed at supporting mathematical proof development on a computer that have laid the groundwork for and eventually have evolved into modern interactive proof assistants. We claim that an important milestone in the development of these systems was the creation of organized libraries accumulating all previously available formalized knowledge in such a way that new works could effectively re-use all previously collected notions. In the case of Mizar, the turning point of its development was the decision to start building the Mizar Mathematical Library as a centrally-managed knowledge base maintained together with the formalization language and the verification system. In this paper we show the process of forming this library, the evolution of its design principles, and also present some data showing its current use with the modern version of the Mizar proof checker, but also as a rich corpus of semantically linked mathematical data in various areas including web-based and natural language proof presentation, maths education, and machine learning based automated theorem proving.

In the paper, we discuss the formal approach to Tarski geometry axioms modelled with the help of the Mizar computerized proof assistant system.Although our basic development was inspired by Julien Narboux's Coq pseudo-code and is dated back to 2014, there are significant steps in the formalization of geometry done in the last decade of the previous century.Taking this into account, we will propose the reuse of existing results within this new framework (including Hilbert's axiomatic approach), with the ultimate future goal to encode the textbook Metamathematische Methoden in der Geometrie by Schwabhäuser, Szmielew and Tarski.We try however to go much further from the use of simple predicates in the direction of the use of structures with their inheritance, attributes as a tool of more human-friendly namespaces for axioms, and registrations of clusters to obtain more automation (with the possible use of external equational theorem provers like Otter/Prover9).

Mathematics, especially algebra, uses plenty of structures: groups, rings, integral domains, fields, vector spaces to name a few of the most basic ones.Classes of structures are closely connected -usually by inclusion -naturally leading to hierarchies that has been reproduced in different forms in different mathematical repositories.In this paper we give a brief overview of some existing algebraic hierarchies and report on the latest developments in the Mizar computerized proof assistant system.In particular we present a detailed algebraic hierarchy that has been defined in Mizar and discuss extensions of the hierarchy towards more involved domains.Taking fully formal approach into account we meet new difficulties comparing with its informal mathematical framework.

Rough sets offer a well-known approach to incomplete or imprecise data. In the paper I briefly report how this framework was successfully encoded by means of one of the leading computer proof-assistants in the world. The general approach is essentially based on binary relations, and all natural pro perties of approximation operators can be obtained via adjectives added to underlying relations. I focus on lattice-theoretical aspects of rough sets to enable the application of external theorem provers like EQP or Prover9 as well as to translate them into TPTP format widely recognized in the world of automated proof search. I wanted to have a clearly written, possibly formal, although informal as a rule, paper authored by a specialist from the discipline another than lattice theory. It appeared that Lattice theory for rough sets by Jouni Järvinen (called LTRS for short) was quite a reasonable choice to be a testbed for the current formalisation both of lattices and of rough sets. A popular computerised proof-assistant Mizar was used as a tool, hence all the efforts are available in one of the largest repositories of computer-checked mathematical knowledge, called Mizar Mathematical Library.

Equality is fundamental notion of logic and mathematics as a whole.If computer-supported formalization of knowledge is taken into account, sooner or later one should precisely declare the intended meaning/interpretation of the primitive predicate symbol of equality.In the paper we draw some issues how computerized proof-assistants can deal with this notion, and at the same time, we propose solutions, which are not contradictory with mathematical tradition and readability of source code.Our discussion is illustrated with examples taken from the implementation of the MIZAR system.

Recently some longstanding open lattice theory problems were solved with the help of automated theorem provers. The question which may be posed is how to cope with such results to improve their presentation for human without loss of machine-readability, not only at the proof level, which should be rather straightforward, but also at the stage of rebuilding appropriate data structure. We describe the framework extending already existed in the Mizar library for Boolean algebras to cover more general cases of lattice with complements. The efficiency of this approach was tested e.g. on short axiom systems for Boolean algebras based on negation and disjunction. We also proved Nachbin theorem for spectra of distributive lattices.

This special issue is dedicated to works related to Mizar , the theorem proving project started by Andrzej Trybulec in the 1970s, and other automated proof checking systems used for formalizing mathematics.

Theory exploration is a term describing the development of a formal approach to selected topic, usually within mathematics or computer science, with the help of an automated proof-assistant. This activity however usually doesn't reflect the view of science considered as a whole, not as separated islands of knowledge. Merging theories essentially has its primary aim of bridging these gaps between specific disciplines. As we provided formal apparatus for basic notions within rough set theory (as e.g. approximation operators and membership functions), we try to reuse the knowledge which is already contained in available repositories of computer-checked mathematical knowledge, or which can be obtained in a relatively easy way. We can point out at least three topics here: topological aspects of rough sets – as approximation operators have properties of the topological interior and closure; possible connections with formal concept analysis; lattice-theoretic approach giving the algebraic viewpoint (e.g. Stone algebras). In the first case, we discovered semiautomatically some connections with Isomichi's classification of subsets of a topological space and with the problem of fourteen Kuratowski sets. This paper is also a brief description of the computer source code which is a feasible illustration of our approach – nearly two thousand lines containing all the formal proofs (essentially we omit them in the paper). In such a way we can give the formal characterization of rough sets in terms of topologies or orders. Although fully formal, still the approach can be revised to keep the uniformity all the time.

The computer certification of rough sets (the translation in a way understandable by machines) seems to be far beyond the test phase. To assure the feasibility of the approach, we try to encode selected problems within rough set theory and as the tes