Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji:
Pełny rekord metadanych
Pole DCWartośćJęzyk
dc.contributor.authorGrabowski, Adampl
dc.identifier.citationFormalized Mathematics, Volume 23, Issue 4, 387–396pl
dc.description.abstractThe 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 a ⩽ b) 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].pl
dc.publisherDe Gruyter Openpl
dc.subjectpseudocomplemented latticespl
dc.subjectStone latticespl
dc.subjectBoolean latticespl
dc.subjectlattice of natural divisorspl
dc.titleStone Latticespl
dc.description.AffiliationInstitute of Informatics, University of Białystok, Ciołkowskiego 1M, 15-245 Białystok, Polandpl
dc.description.referencesGrzegorz Bancerek. Cardinal numbers. Formalized Mathematics, 1(2):377–382,
dc.description.referencesGrzegorz Bancerek. Filters – part II. Quotient lattices modulo filters and direct product of two lattices. Formalized Mathematics, 2(3):433–438,
dc.description.referencesGrzegorz Bancerek. Ideals. Formalized Mathematics, 5(2):149–156,
dc.description.referencesGrzegorz Bancerek. Complete lattices. Formalized Mathematics, 2(5):719–725,
dc.description.referencesGrzegorz Bancerek. The ordinal numbers. Formalized Mathematics, 1(1):91–96,
dc.description.referencesGrzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, Karol Pąk, and Josef Urban. Mizar: State-of-the-art and beyond. In Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge, editors, Intelligent Computer Mathematics, volume 9150 of Lecture Notes in Computer Science, pages 261–279. Springer International Publishing, 2015. ISBN 978-3-319-20614-1. doi:10.1007/978-3-319-20615-8 17. [Crossref]pl
dc.description.referencesCzesław Byliński. Some basic properties of sets. Formalized Mathematics, 1(1):47–53,
dc.description.referencesMarek Chmur. The lattice of natural numbers and the sublattice of it. The set of prime numbers. Formalized Mathematics, 2(4):453–459,
dc.description.referencesAgata Darmochwał. Finite sets. Formalized Mathematics, 1(1):165–167,
dc.description.referencesAdam Grabowski. On the computer-assisted reasoning about rough sets. In B. Dunin-Kęplicz, A. Jankowski, A. Skowron, and M. Szczuka, editors, International Workshop on Monitoring, Security, and Rescue Techniques in Multiagent Systems Location, volume 28 of Advances in Soft Computing, pages 215–226, Berlin, Heidelberg, 2005. Springer-Verlag. doi:10.1007/3-540-32370-8 15. [Crossref]pl
dc.description.referencesAdam Grabowski. Efficient rough set theory merging. Fundamenta Informaticae, 135(4): 371–385, 2014. doi:10.3233/FI-2014-1129. [Crossref] [Web of Science]pl
dc.description.referencesAdam Grabowski. Mechanizing complemented lattices within Mizar system. Journal of Automated Reasoning, 55:211–221, 2015. doi:10.1007/s10817-015-9333-5. [Crossref]pl
dc.description.referencesAdam Grabowski. Prime filters and ideals in distributive lattices. Formalized Mathematics, 21(3):213–221, 2013. doi:10.2478/forma-2013-0023. [Crossref]pl
dc.description.referencesAdam Grabowski. On square-free numbers. Formalized Mathematics, 21(2):153–162, 2013. doi:10.2478/forma-2013-0017. [Crossref]pl
dc.description.referencesAdam Grabowski. Two axiomatizations of Nelson algebras. Formalized Mathematics, 23 (2):115–125, 2015. doi:10.1515/forma-2015-0012. [Crossref]pl
dc.description.referencesAdam Grabowski and Magdalena Jastrzębska. Rough set theory from a math-assistant perspective. In Rough Sets and Intelligent Systems Paradigms, International Conference, RSEISP 2007, Warsaw, Poland, June 28–30, 2007, Proceedings, pages 152–161, 2007. doi:10.1007/978-3-540-73451-2 17. [Crossref]pl
dc.description.referencesGeorge Grätzer. Lattice Theory: Foundation. Birkhäuser,
dc.description.referencesGeorge Grätzer and E.T. Schmidt. On a problem of M.H. Stone. Acta Mathematica Academiae Scientarum Hungaricae, (8):455–460,
dc.description.referencesJouni Järvinen. Lattice theory for rough sets. Transactions of Rough Sets, VI, Lecture Notes in Computer Science, 4374:400–498,
dc.description.referencesMagdalena Jastrzębska and Adam Grabowski. On the properties of the Möbius function. Formalized Mathematics, 14(1):29–36, 2006. doi:10.2478/v10037-006-0005-0. [Crossref]pl
dc.description.referencesJolanta Kamieńska and Jarosław Stanisław Walijewski. Homomorphisms of lattices, finite join and finite meet. Formalized Mathematics, 4(1):35–40,
dc.description.referencesRafał Kwiatek. Factorial and Newton coefficients. Formalized Mathematics, 1(5):887–890,
dc.description.referencesRafał Kwiatek and Grzegorz Zwara. The divisibility of integers and integer relatively primes. Formalized Mathematics, 1(5):829–832,
dc.description.referencesRobert Milewski. More on the lattice of many sorted equivalence relations. Formalized Mathematics, 5(4):565–569,
dc.description.referencesAndrzej Trybulec. Enumerated sets. Formalized Mathematics, 1(1):25–34,
dc.description.referencesMichał J. Trybulec. Integers. Formalized Mathematics, 1(3):501–505,
dc.description.referencesZinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67–71,
dc.description.referencesStanisław Żukowski. Introduction to lattice theory. Formalized Mathematics, 1(1):215–222,
Występuje w kolekcji(ach):Artykuły naukowe (WInf)
Formalized Mathematics, 2015, Volume 23, Issue 4

Pliki w tej pozycji:
Plik Opis RozmiarFormat 
forma-2015-0031.pdf280,64 kBAdobe PDFOtwórz
Pokaż uproszczony widok rekordu Zobacz statystyki

Pozycja ta dostępna jest na podstawie licencji Licencja Creative Commons CCL Creative Commons