REPOZYTORIUM UNIWERSYTETU
W BIAŁYMSTOKU

Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji: `http://hdl.handle.net/11320/4876`
 Tytuł: Two Axiomatizations of Nelson Algebras Autorzy: Grabowski, Adam Słowa kluczowe: quasi-pseudo-Boolean algebrasNelson latticesde Morgan lattices Data wydania: 2015 Data dodania: 15-gru-2016 Wydawca: De Gruyter Open Źródło: Formalized Mathematics, Volume 23, Issue 2, 115–125 Abstrakt: Nelson algebras were first studied by Rasiowa and Białynicki- Birula [1] under the name N-lattices or quasi-pseudo-Boolean algebras. Later, in investigations by Monteiro and Brignole [3, 4], and [2] the name “Nelson algebras” was adopted - which is now commonly used to show the correspondence with Nelson’s paper [14] on constructive logic with strong negation. By a Nelson algebra we mean an abstract algebra 〈L, T, -, ¬, →, ⇒, ⊔, ⊓〉where L is the carrier, − is a quasi-complementation (Rasiowa used the sign ~, but in Mizar “−” should be used to follow the approach described in [12] and [10]), ¬ is a weak pseudo-complementation → is weak relative pseudocomplementation and ⇒ is implicative operation. ⊔ and ⊓ are ordinary lattice binary operations of supremum and infimum. In this article we give the definition and basic properties of these algebras according to [16] and [15]. We start with preliminary section on quasi-Boolean algebras (i.e. de Morgan bounded lattices). Later we give the axioms in the form of Mizar adjectives with names corresponding with those in [15]. As our main result we give two axiomatizations (non-equational and equational) and the full formal proof of their equivalence. The second set of equations is rather long but it shows the logical essence of Nelson lattices. This formalization aims at the construction of algebraic model of rough sets [9] in our future submissions. Section 4 contains all items from Th. 1.2 and 1.3 (and the itemization is given in the text). In the fifth section we provide full formal proof of Th. 2.1 p. 75 [16]. Afiliacja: Institute of Informatics, University of Białystok, Ciołkowskiego 1M, 15-245 Białystok, Poland URI: http://hdl.handle.net/11320/4876 DOI: 10.1515/forma-2015-0012 ISSN: 1426-26301898-9934 Typ Dokumentu: Article Występuje w kolekcji(ach): Artykuły naukowe (WMiI)Formalized Mathematics, 2015, Volume 23, Issue 2

Pliki w tej pozycji:
Plik Opis RozmiarFormat