Search Results

You are looking at 1 - 10 of 32 items for

  • Author: Adam Grabowski x
Clear All Modify Search
Open access

Adam Grabowski

Summary

Rough sets, developed by Pawlak, are an important model of incomplete or partially known information. In this article, which is essentially a continuation of [11], we characterize rough sets in terms of topological closure and interior, as the approximations have the properties of the Kuratowski operators. We decided to merge topological spaces with tolerance approximation spaces. As a testbed for our developed approach, we restated the results of Isomichi [13] (formalized in Mizar in [14]) and about fourteen sets of Kuratowski [17] (encoded with the help of Mizar adjectives and clusters’ registrations in [1]) in terms of rough approximations. The upper bounds which were 14 and 7 in the original paper of Kuratowski, in our case are six and three, respectively.

It turns out that within the classification given by Isomichi, 1st class subsets are precisely crisp sets, 2nd class subsets are proper rough sets, and there are no 3rd class subsets in topological spaces generated by approximations. Also the important results about these spaces is that they are extremally disconnected [15], hence lattices of their domains are Boolean.

Furthermore, we develop the theory of abstract spaces equipped with maps possessing characteristic properties of rough approximations which enables us to freely use the notions from the theory of rough sets and topological spaces formalized in the Mizar Mathematical Library [10].

Open access

Adam Grabowski

Summary

In this article, we continue the development of the theory of fuzzy sets [23], started with [14] with the future aim to provide the formalization of fuzzy numbers [8] in terms reflecting the current state of the Mizar Mathematical Library. Note that in order to have more usable approach in [14], we revised that article as well; some of the ideas were described in [12]. As we can actually understand fuzzy sets just as their membership functions (via the equality of membership function and their set-theoretic counterpart), all the calculations are much simpler. To test our newly proposed approach, we give the notions of (normal) triangular and trapezoidal fuzzy sets as the examples of concrete fuzzy objects. Also -cuts, the core of a fuzzy set, and normalized fuzzy sets were defined. Main technical obstacle was to prove continuity of the glued maps, and in fact we did this not through its topological counterpart, but extensively reusing properties of the real line (with loss of generality of the approach, though), because we aim at formalizing fuzzy numbers in our future submissions, as well as merging with rough set approach as introduced in [13] and [11]. Our base for formalization was [9] and [10].

Open access

Adam Grabowski

Summary.

The article continues the formalization of the lattice theory (as structures with two binary operations, not in terms of ordering relations). In the Mizar Mathematical Library, there are some attempts to formalize prime ideals and filters; one series of articles written as decoding [9] proven some results; we tried however to follow [21], [12], and [13]. All three were devoted to the Stone representation theorem [18] for Boolean or Heyting lattices. The main aim of the present article was to bridge this gap between general distributive lattices and Boolean algebras, having in mind that the more general approach will eventually replace the common proof of aforementioned articles.1

Because in Boolean algebras the notions of ultrafilters, prime filters and maximal filters coincide, we decided to construct some concrete examples of ultrafilters in nontrivial Boolean lattice. We proved also the Prime Ideal Theorem not as BPI (Boolean Prime Ideal), but in the more general setting.

In the final section we present Nachbin theorems [15],[1] expressed both in terms of maximal and prime filters and as the unordered spectra of a lattice [11], [10]. This shows that if the notion of maximal and prime filters coincide in the lattice, it is Boolean.

Open access

Adam Grabowski

Summary

The article continues the formalization of the lattice theory (as structures with two binary operations, not in terms of ordering relations). In the paper, the notion of a pseudocomplement in a lattice is formally introduced in Mizar, and based on this we define the notion of the skeleton and the set of dense elements in a pseudocomplemented lattice, giving the meet-decomposition of arbitrary element of a lattice as the infimum of two elements: one belonging to the skeleton, and the other which is dense.

The core of the paper is of course the idea of Stone identity

a*a**=T,
which is fundamental for us: Stone lattices are those lattices L, which are distributive, bounded, and satisfy Stone identity for all elements a ∈ L. Stone algebras were introduced by Grätzer and Schmidt in [18]. Of course, the pseudocomplement is unique (if exists), so in a pseudcomplemented lattice we defined a * as the Mizar functor (unary operation mapping every element to its pseudocomplement). In Section 2 we prove formally a collection of ordinary properties of pseudocomplemented lattices.

All Boolean lattices are Stone, and a natural example of the lattice which is Stone, but not Boolean, is the lattice of all natural divisors of p 2 for arbitrary prime number p (Section 6). At the end we formalize the notion of the Stone lattice B [2] (of pairs of elements a, b of B such that ab) constructed as a sublattice of B 2, where B is arbitrary Boolean algebra (and we describe skeleton and the set of dense elements in such lattices). In a natural way, we deal with Cartesian product of pseudocomplemented lattices.

Our formalization was inspired by [17], and is an important step in formalizing Jouni Järvinen Lattice theory for rough sets [19], so it follows rather the latter paper. We deal essentially with Section 4.3, pages 423–426. The description of handling complemented structures in Mizar [6] can be found in [12]. The current article together with [15] establishes the formal background for algebraic structures which are important for [10], [16] by means of mechanisms of merging theories as described in [11].

Open access

Adam Grabowski

Summary

In the article the formal characterization of square-free numbers is shown; in this manner the paper is the continuation of [19]. Essentially, we prepared some lemmas for convenient work with numbers (including the proof that the sequence of prime reciprocals diverges [1]) according to [18] which were absent in the Mizar Mathematical Library. Some of them were expressed in terms of clusters’ registrations, enabling automatization machinery available in the Mizar system. Our main result of the article is in the final section; we proved that the lattice of positive divisors of a positive integer n is Boolean if and only if n is square-free.

Open access

Adam Grabowski

Nelson algebras were first studied by Rasiowa and Białynicki- Birula [1] under the name N-lattices or quasi-pseudo-Boolean algebras. Later, in investigations by Monteiro and Brignole [3, 4], and [2] the name “Nelson algebras” was adopted - which is now commonly used to show the correspondence with Nelson’s paper [14] on constructive logic with strong negation.

By a Nelson algebra we mean an abstract algebra

〈L, T, -, ¬, →, ⇒, ⊔, ⊓〉

where L is the carrier, − is a quasi-complementation (Rasiowa used the sign ~, but in Mizar “−” should be used to follow the approach described in [12] and [10]), ¬ is a weak pseudo-complementation → is weak relative pseudocomplementation and ⇒ is implicative operation. ⊔ and ⊓ are ordinary lattice binary operations of supremum and infimum.

In this article we give the definition and basic properties of these algebras according to [16] and [15]. We start with preliminary section on quasi-Boolean algebras (i.e. de Morgan bounded lattices). Later we give the axioms in the form of Mizar adjectives with names corresponding with those in [15]. As our main result we give two axiomatizations (non-equational and equational) and the full formal proof of their equivalence.

The second set of equations is rather long but it shows the logical essence of Nelson lattices. This formalization aims at the construction of algebraic model of rough sets [9] in our future submissions. Section 4 contains all items from Th. 1.2 and 1.3 (and the itemization is given in the text). In the fifth section we provide full formal proof of Th. 2.1 p. 75 [16].

Open access

Adam Grabowski

Summary

The notion of a rough set, developed by Pawlak [10], is an important tool to describe situation of incomplete or partially unknown information. In this article, which is essentially the continuation of [6], we try to give the characterization of approximation operators in terms of ordinary properties of underlying relations (some of them, as serial and mediate relations, were not available in the Mizar Mathematical Library). Here we drop the classical equivalence- and tolerance-based models of rough sets [12] trying to formalize some parts of [19] following also [18] in some sense (Propositions 1-8, Corr. 1 and 2; the complete description is available in the Mizar script). Our main problem was that informally, there is a direct correspondence between relations and underlying properties, in our approach however [7], which uses relational structures rather than relations, we had to switch between classical (based on pure set theory) and abstract (using the notion of a structure) parts of the Mizar Mathematical Library. Our next step will be translation of these properties into the pure language of Mizar attributes.

Open access

Adam Grabowski

Summary

In the article the formal characterization of triangular numbers (famous from [15] and words “EYPHKA! num = Δ+Δ+Δ”) [17] is given. Our primary aim was to formalize one of the items (#42) from Wiedijk’s Top 100 Mathematical Theorems list [33], namely that the sequence of sums of reciprocals of triangular numbers converges to 2. This Mizar representation was written in 2007. As the Mizar language evolved and attributes with arguments were implemented, we decided to extend these lines and we characterized polygonal numbers. We formalized centered polygonal numbers, the connection between triangular and square numbers, and also some equalities involving Mersenne primes and perfect numbers. We gave also explicit formula to obtain from the polygonal number its ordinal index. Also selected congruences modulo 10 were enumerated. Our work basically covers the Wikipedia item for triangular numbers and the Online Encyclopedia of Integer Sequences (http://oeis.org/A000217). An interesting related result [16] could be the proof of Lagrange’s four-square theorem or Fermat’s polygonal number theorem [32].

Open access

Adam Grabowski

Summary

Almost Distributive Lattices (ADL) are structures defined by Swamy and Rao [14] as a common abstraction of some generalizations of the Boolean algebra. In our paper, we deal with a certain further generalization of ADLs, namely the Generalized Almost Distributive Lattices (GADL). Our main aim was to give the formal counterpart of this structure and we succeeded formalizing all items from the Section 3 of Rao et al.’s paper [13]. Essentially among GADLs we can find structures which are neither V-commutative nor Λ-commutative (resp., Λ-commutative); consequently not all forms of absorption identities hold.

We characterized some necessary and sufficient conditions for commutativity and distributivity, we also defined the class of GADLs with zero element. We tried to use as much attributes and cluster registrations as possible, hence many identities are expressed in terms of adjectives; also some generalizations of wellknown notions from lattice theory [11] formalized within the Mizar Mathematical Library were proposed. Finally, some important examples from Rao’s paper were introduced. We construct the example of GADL which is not an ADL. Mechanization of proofs in this specific area could be a good starting point towards further generalization of lattice theory [10] with the help of automated theorem provers [8].

Open access

Adam Grabowski

Summary

The purpose of this paper was to prove formally, using the Mizar language, Arithmetic Mean/Geometric Mean theorem known maybe better under the name of AM-GM inequality or Cauchy mean theorem. It states that the arithmetic mean of a list of a non-negative real numbers is greater than or equal to the geometric mean of the same list.

The formalization was tempting for at least two reasons: one of them, perhaps the strongest, was that the proof of this theorem seemed to be relatively easy to formalize (e.g. the weaker variant of this was proven in [13]). Also Jensen’s inequality is already present in the Mizar Mathematical Library. We were impressed by the beauty and elegance of the simple proof by induction and so we decided to follow this specific way.

The proof follows similar lines as that written in Isabelle [18]; the comparison of both could be really interesting as it seems that in both systems the number of lines needed to prove this are really close.

This theorem is item #38 from the “Formalizing 100 Theorems” list maintained by Freek Wiedijk at http://www.cs.ru.nl/F.Wiedijk/100/.