REPOZYTORIUM UNIWERSYTETU
W BIAŁYMSTOKU
UwB

  1. Repozytorium Uniwersytetu w Białymstoku
  2. Czasopisma naukowe / Journals
  3. Formalized Mathematics
  4. Formalized Mathematics, 2020, Volume 28, Issue 2

Szukanie zaawansowane
  • Zespoły i Kolekcje


  • Zaloguj się
  • Zarejestruj się
  • Mój RUB
  • FAQ
  • Polityka
  • Regulamin
  • DOI
  • Instrukcja
  • Aspekty prawne
  • Open Access
  • Archiwum


  • Kontakt
  • O Dspace
  • Strona Biblioteki
  • Strona Uczelni



    • Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji: http://hdl.handle.net/11320/10838
    Pełny rekord metadanych
    Pole DCWartośćJęzyk
    dc.contributor.authorKulesza, Dominik-
    dc.contributor.authorGrabowski, Adam-
    dc.date.accessioned2021-05-04T09:47:00Z-
    dc.date.available2021-05-04T09:47:00Z-
    dc.date.issued2020-
    dc.identifier.citationFormalized Mathematics, Volume 28, Issue 2, Pages 217-225pl
    dc.identifier.issn1426-2630-
    dc.identifier.urihttp://hdl.handle.net/11320/10838-
    dc.description.abstractThe main aim of this article is to introduce formally one of the generalizations of lattices, namely quasilattices, which can be obtained from the axiomatization of the former class by certain weakening of ordinary absorption laws. We show propositions QLT-1 to QLT-7 from [15], presenting also some short variants of corresponding axiom systems. Some of the results were proven in the Mizar [1], [2] system with the help of Prover9 [14] proof assistant.pl
    dc.language.isoenpl
    dc.publisherDeGruyter Openpl
    dc.rightsAttribution-ShareAlike 3.0 Unported (CC BY-SA 3.0)-
    dc.rights.urihttps://creativecommons.org/licenses/by-sa/3.0/-
    dc.subjectlattice theorypl
    dc.subjectquasilatticepl
    dc.subjectabsorption lawpl
    dc.titleFormalization of Quasilatticespl
    dc.typeArticlepl
    dc.rights.holder© 2020 University of Białymstoku;-
    dc.rights.holderCC-BY-SA License ver. 3.0 or later;-
    dc.identifier.doi10.2478/forma-2020-0019-
    dc.description.AffiliationDominik Kulesza - Institute of Informatics, University of Białystok, Polandpl
    dc.description.AffiliationAdam Grabowski - Institute of Informatics, University of Białystok, Polandpl
    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.pl
    dc.description.referencesGrzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, and Karol Pąk. The role of the Mizar Mathematical Library for interactive proof development in Mizar. Journal of Automated Reasoning, 61(1):9–32, 2018. doi:10.1007/s10817-017-9440-6.pl
    dc.description.referencesGarrett Birkhoff. Lattice Theory. Providence, Rhode Island, New York, 1967.pl
    dc.description.referencesB.A. Davey and H.A. Priestley. Introduction to Lattices and Order. Cambridge University Press, 2002.pl
    dc.description.referencesG. Gierz, K.H. Hofmann, K. Keimel, J.D. Lawson, M. Mislove, and D.S. Scott. A Compendium of Continuous Lattices. Springer-Verlag, Berlin, Heidelberg, New York, 1980.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.pl
    dc.description.referencesAdam Grabowski and Robert Milewski. Boolean posets, posets under inclusion and products of relational structures. Formalized Mathematics, 6(1):117–121, 1997.pl
    dc.description.referencesAdam Grabowski and Markus Moschner. Managing heterogeneous theories within a mathematical knowledge repository. In Andrea Asperti, Grzegorz Bancerek, and Andrzej Trybulec, editors, Mathematical Knowledge Management Proceedings, volume 3119 of Lecture Notes in Computer Science, pages 116–129. Springer, 2004. doi:10.1007/978-3-540-27818-4_9. 3rd International Conference on Mathematical Knowledge Management, Bialowieza, Poland, Sep. 19–21, 2004.pl
    dc.description.referencesAdam Grabowski and Damian Sawicki. On two alternative axiomatizations of lattices by McKenzie and Sholander. Formalized Mathematics, 26(2):193–198, 2018. doi:10.2478/forma-2018-0017.pl
    dc.description.referencesAdam Grabowski and Christoph Schwarzweller. Translating mathematical vernacular into knowledge repositories. In Michael Kohlhase, editor, Mathematical Knowledge Management, volume 3863 of Lecture Notes in Computer Science, pages 49–64. Springer, 2006. doi:https://doi.org/10.1007/11618027_4. 4th International Conference on Mathematical Knowledge Management, Bremen, Germany, MKM 2005, July 15–17, 2005, Revised Selected Papers.pl
    dc.description.referencesAdam Grabowski, Artur Korniłowicz, and Christoph Schwarzweller. Equality in computer proof-assistants. In Ganzha, Maria and Maciaszek, Leszek and Paprzycki, Marcin, editor, Proceedings of the 2015 Federated Conference on Computer Science and Information Systems, volume 5 of ACSIS-Annals of Computer Science and Information Systems, pages 45–54. IEEE, 2015. doi:10.15439/2015F229.pl
    dc.description.referencesGeorge Grätzer. General Lattice Theory. Academic Press, New York, 1978.pl
    dc.description.referencesGeorge Grätzer. Lattice Theory: Foundation. Birkhäuser, 2011.pl
    dc.description.referencesWilliam McCune. Prover9 and Mace4. 2005–2010.pl
    dc.description.referencesWilliam McCune and Ranganathan Padmanabhan. Automated Deduction in Equational Logic and Cubic Curves. Springer-Verlag, Berlin, 1996.pl
    dc.description.referencesRanganathan Padmanabhan and Sergiu Rudeanu. Axioms for Lattices and Boolean Algebras. World Scientific Publishers, 2008.pl
    dc.description.referencesPiotr Rudnicki and Josef Urban. Escape to ATP for Mizar. In First International Workshop on Proof eXchange for Theorem Proving-PxTP 2011, 2011.pl
    dc.description.referencesStanisław Żukowski. Introduction to lattice theory. Formalized Mathematics, 1(1):215–222, 1990.pl
    dc.identifier.eissn1898-9934-
    dc.description.volume28pl
    dc.description.issue2pl
    dc.description.firstpage217pl
    dc.description.lastpage225pl
    dc.identifier.citation2Formalized Mathematicspl
    dc.identifier.orcidbrakorcid-
    dc.identifier.orcid0000-0001-5026-3990-
    Występuje w kolekcji(ach):Artykuły naukowe (WInf)
    Formalized Mathematics, 2020, Volume 28, Issue 2

    Pliki w tej pozycji:
    Plik Opis RozmiarFormat 
    10.2478_forma-2020-0019.pdf244,1 kBAdobe PDFOtwórz
    Pokaż uproszczony widok rekordu Zobacz statystyki


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