http://hdl.handle.net/11320/3662 2026-06-01T16:28:40Z 2026-06-01T16:28:40Z Grabowski, Adam http://hdl.handle.net/11320/3690 2017-10-05T22:56:47Z 2013-01-01T00:00:00Z

Tytuł: Prime Filters and Ideals in Distributive Lattices Autorzy: Grabowski, Adam Abstrakt: 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.

2013-01-01T00:00:00Z Yamazaki, Hiroshi Okazaki, Hiroyuki Nakasho, Kazuhisa Shidama, Yasunari http://hdl.handle.net/11320/3689 2017-10-05T22:56:46Z 2013-01-01T00:00:00Z

Tytuł: Isomorphisms of Direct Products of Cyclic Groups of Prime Power Order Autorzy: Yamazaki, Hiroshi; Okazaki, Hiroyuki; Nakasho, Kazuhisa; Shidama, Yasunari Abstrakt: In this paper we formalized some theorems concerning the cyclic groups of prime power order. We formalize that every commutative cyclic group of prime power order is isomorphic to a direct product of family of cyclic groups [1], [18].

2013-01-01T00:00:00Z Niewiadomska, Eliza Grabowski, Adam http://hdl.handle.net/11320/3691 2017-10-05T22:57:30Z 2013-01-01T00:00:00Z

Tytuł: Introduction to Formal Preference Spaces Autorzy: Niewiadomska, Eliza; Grabowski, Adam Abstrakt: In the article the formal characterization of preference spaces [1] is given. As the preference relation is one of the very basic notions of mathematical economics [9], it prepares some ground for a more thorough formalization of consumer theory (although some work has already been done - see [17]). There was an attempt to formalize similar results in Mizar, but this work seems still unfinished [18]. There are many approaches to preferences in literature. We modelled them in a rather illustrative way (similar structures were considered in [8]): either the consumer (strictly) prefers an alternative, or they are of equal interest; he/she could also have no opinion of the choice. Then our structures are based on three relations on the (arbitrary, not necessarily finite) set of alternatives. The completeness property can however also be modelled, although we rather follow [2] which is more general [12]. Additionally we assume all three relations are disjoint and their set-theoretic union gives a whole universe of alternatives. We constructed some positive and negative examples of preference structures; the main aim of the article however is to give the characterization of consumer preference structures in terms of a binary relation, called characteristic relation [10], and to show the way the corresponding structure can be obtained only using this relation. Finally, we show the connection between tournament and total spaces and usual properties of the ordering relations.

2013-01-01T00:00:00Z Arai, Kenichi Okazaki, Hiroyuki http://hdl.handle.net/11320/3686 2017-10-05T22:56:47Z 2013-01-01T00:00:00Z

Tytuł: Formalization of the Advanced Encryption Standard. Part I Autorzy: Arai, Kenichi; Okazaki, Hiroyuki Abstrakt: In this article, we formalize the Advanced Encryption Standard (AES). AES, which is the most widely used symmetric cryptosystem in the world, is a block cipher that was selected by the National Institute of Standards and Technology (NIST) as an official Federal Information Processing Standard for the United States in 2001 [12]. AES is the successor to DES [13], which was formerly the most widely used symmetric cryptosystem in the world. We formalize the AES algorithm according to [12]. We then verify the correctness of the formalized algorithm that the ciphertext encoded by the AES algorithm can be decoded uniquely by the same key. Please note the following points about this formalization: the AES round process is composed of the SubBytes, ShiftRows, MixColumns, and AddRoundKey transformations (see [12]). In this formalization, the SubBytes and MixColumns transformations are given as permutations, because it is necessary to treat the finite field GF(28) for those transformations. The formalization of AES that considers the finite field GF(28) is formalized by the future article.

2013-01-01T00:00:00Z