http://hdl.handle.net/11320/7636 Sat, 20 Jun 2026 14:59:47 GMT 2026-06-20T14:59:47Z http://hdl.handle.net/11320/7639 Tytuł: Zariski Topology Autorzy: Watase, Yasushige Abstrakt: We formalize in the Mizar system [3], [4] basic definitions of commutative ring theory such as prime spectrum, nilradical, Jacobson radical, local ring, and semi-local ring [5], [6], then formalize proofs of some related theorems along with the first chapter of [1].The article introduces the so-called Zariski topology. The set of all prime ideals of a commutative ring A is called the prime spectrum of A denoted by Spectrum A. A new functor Spec generates Zariski topology to make Spectrum A a topological space. A different role is given to Spec as a map from a ring morphism of commutative rings to that of topological spaces by the following manner: for a ring homomorphism h : A → B, we defined (Spec h) : Spec B → Spec A by (Spec h)(𝔭) = h−1(𝔭) where 𝔭 2 Spec B. Mon, 01 Jan 2018 00:00:00 GMT http://hdl.handle.net/11320/7639 2018-01-01T00:00:00Z http://hdl.handle.net/11320/7638 Tytuł: Fundamental Properties of Fuzzy Implications Autorzy: Grabowski, Adam Abstrakt: In the article we continue in the Mizar system [8], [2] the formalization of fuzzy implications according to the monograph of Baczyński and Jayaram “Fuzzy Implications” [1]. We develop a framework of Mizar attributes allowing us for a smooth proving of basic properties of these fuzzy connectives [9]. We also give a set of theorems about the ordering of nine fundamental implications: Łukasiewicz (ILK), Gödel (IGD), Reichenbach (IRC), Kleene-Dienes (IKD), Goguen (IGG), Rescher (IRS), Yager (IYG), Weber (IWB), and Fodor (IFD).This work is a continuation of the development of fuzzy sets in Mizar [6]; it could be used to give a variety of more general operations on fuzzy sets [13]. The formalization follows [10], [5], and [4]. Mon, 01 Jan 2018 00:00:00 GMT http://hdl.handle.net/11320/7638 2018-01-01T00:00:00Z http://hdl.handle.net/11320/7637 Tytuł: Pythagorean Tuning: Pentatonic and Heptatonic Scale Autorzy: Coghetto, Roland Abstrakt: In this article, using the Mizar system [3], [4], we define a structure [1], [6] in order to build a Pythagorean pentatonic scale and a Pythagorean heptatonic scale1 [5], [7]. Mon, 01 Jan 2018 00:00:00 GMT http://hdl.handle.net/11320/7637 2018-01-01T00:00:00Z