Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji:
http://hdl.handle.net/11320/12387
Pełny rekord metadanych
Pole DC | Wartość | Język |
---|---|---|
dc.contributor.author | Sawicki, Damian | - |
dc.contributor.author | Grabowski, Adam | - |
dc.date.accessioned | 2022-01-03T13:33:16Z | - |
dc.date.available | 2022-01-03T13:33:16Z | - |
dc.date.issued | 2021 | - |
dc.identifier.citation | Formalized Mathematics, Volume 29, Issue 2, Pages 77-85 | pl |
dc.identifier.issn | 1426-2630 | - |
dc.identifier.uri | http://hdl.handle.net/11320/12387 | - |
dc.description.abstract | The main aim of this article is to introduce formally two generalizations of lattices, namely weakly associative lattices and near lattices, which can be obtained from the former by certain weakening of the usual well-known axioms. We show selected propositions devoted to weakly associative lattices and near lattices from Chapter 6 of [15], dealing also with alternative versions of classical axiomatizations. Some of the results were proven in the Mizar [1], [2] system with the help of Prover9 [14] proof assistant. | pl |
dc.language.iso | en | pl |
dc.publisher | DeGruyter Open | pl |
dc.rights | Attribution-ShareAlike 3.0 Unported (CC BY-SA 3.0) | - |
dc.rights.uri | https://creativecommons.org/licenses/by-sa/3.0/ | - |
dc.subject | weakly associative lattice | pl |
dc.subject | near lattice | pl |
dc.title | On Weakly Associative Lattices and Near Lattices | pl |
dc.type | Article | pl |
dc.rights.holder | © 2021 University of Białymstoku | pl |
dc.rights.holder | CC-BY-SA License ver. 3.0 or later | pl |
dc.identifier.doi | 10.2478/forma-2021-0008 | - |
dc.description.Affiliation | Damian Sawicki - Institute of Informatics, University of Białystok, Poland | pl |
dc.description.Affiliation | Adam Grabowski - Institute of Informatics, University of Białystok, Poland | pl |
dc.description.references | Grzegorz Bancerek, Czesław Bylinski, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, Karol Pak, 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.references | Grzegorz Bancerek, Czesław Bylinski, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, and Karol Pak. 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.references | Garrett Birkhoff. Lattice Theory. Providence, Rhode Island, New York, 1967. | pl |
dc.description.references | B.A. Davey and H.A. Priestley. Introduction to Lattices and Order. Cambridge University Press, 2002. | pl |
dc.description.references | Ervin Fried and George Grätzer. Some examples of weakly associative lattices. Colloquium Mathematicum, 27:215–221, 1973. doi:10.4064/cm-27-2-215-221. | pl |
dc.description.references | Adam 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.references | Adam 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.references | Adam 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.references | Adam 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.references | Adam 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.references | George Grätzer. General Lattice Theory. Academic Press, New York, 1978. | pl |
dc.description.references | George Grätzer. Lattice Theory: Foundation. Birkhäuser, 2011. | pl |
dc.description.references | Dominik Kulesza and Adam Grabowski. Formalization of quasilattices. Formalized Mathematics, 28(2):217–225, 2020. doi:10.2478/forma-2020-0019. | pl |
dc.description.references | William McCune. Prover9 and Mace4. 2005–2010. | pl |
dc.description.references | William McCune and Ranganathan Padmanabhan. Automated Deduction in Equational Logic and Cubic Curves. Springer-Verlag, Berlin, 1996. | pl |
dc.description.references | Ranganathan Padmanabhan and Sergiu Rudeanu. Axioms for Lattices and Boolean Algebras. World Scientific Publishers, 2008. | pl |
dc.description.references | Piotr 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.references | Stanisław Zukowski. Introduction to lattice theory. Formalized Mathematics, 1(1):215–222, 1990. | pl |
dc.identifier.eissn | 1898-9934 | - |
dc.description.volume | 29 | pl |
dc.description.issue | 2 | pl |
dc.description.firstpage | 77 | pl |
dc.description.lastpage | 85 | pl |
dc.identifier.citation2 | Formalized Mathematics | pl |
dc.identifier.orcid | brakorcid | - |
dc.identifier.orcid | 0000-0001-5026-3990 | - |
Występuje w kolekcji(ach): | Artykuły naukowe (WInf) Formalized Mathematics, 2021, Volume 29, Issue 2 |
Pliki w tej pozycji:
Plik | Opis | Rozmiar | Format | |
---|---|---|---|---|
10.2478_forma-2021-0008.pdf | 239,73 kB | Adobe PDF | Otwórz |
Pozycja ta dostępna jest na podstawie licencji Licencja Creative Commons CCL