REPOZYTORIUM UNIWERSYTETU
W BIAŁYMSTOKU
UwB

Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji: http://hdl.handle.net/11320/9018
Tytuł: AIM Loops and the AIM Conjecture
Autorzy: Brown, Chad E.
Pąk, Karol
Słowa kluczowe: loops
Abelian inner mapping
groups
Data wydania: 2019
Data dodania: 20-kwi-2020
Wydawca: DeGruyter Open
Źródło: Formalized Mathematics, Volume 27, Issue 4, Pages 321-335
Abstrakt: In this article, we prove, using the Mizar [2] formalism, a number of properties that correspond to the AIM Conjecture. In the first section, we define division operations on loops, inner mappings T, L and R, commutators and associators and basic attributes of interest. We also consider subloops and homomorphisms. Particular subloops are the nucleus and center of a loop and kernels of homomorphisms. Then in Section 2, we define a set Mlt Q of multiplicative mappings of Q and cosets (mostly following Albert 1943 for cosets [1]). Next, in Section 3 we define the notion of a normal subloop and construct quotients by normal subloops. In the last section we define the set InnAut of inner mappings of Q, define the notion of an AIM loop and relate this to the conditions on T, L, and R defined by satisfies TT, etc. We prove in Theorem (67) that the nucleus of an AIM loop is normal and finally in Theorem (68) that the AIM Conjecture follows from knowing every AIM loop satisfies aa1, aa2, aa3, Ka, aK1, aK2 and aK3. The formalization follows M.K. Kinyon, R. Veroff, P. Vojtechovsky [4] (in [3]) as well as Veroff’s Prover9 files.
Afiliacja: Chad E. Brown - Český Institut Informatiky Robotiky a Kybernetiky, Zikova 4, 166 36 Praha 6, Czech Republic
Karol Pąk - Institute of Informatics, University of Białystok, Poland
Sponsorzy: This work has been supported by the European Research Council (ERC) Consolidator grant nr. 649043 AI4REASON and the Polish National Science Centre granted by decision no. DEC-2015/19/D/ST6/01473.
URI: http://hdl.handle.net/11320/9018
DOI: 10.2478/forma-2019-0027
ISSN: 1426-2630
e-ISSN: 1898-9934
metadata.dc.identifier.orcid: brakorcid
0000-0002-7099-1669
Typ Dokumentu: Article
metadata.dc.rights.uri: http://creativecommons.org/licenses/by-sa/3.0/pl/
Występuje w kolekcji(ach):Artykuły naukowe (IInf)
Formalized Mathematics, 2019, Volume 27, Issue 4

Pliki w tej pozycji:
Plik Opis RozmiarFormat 
forma_2019_27_4_0027.pdf291,42 kBAdobe PDFOtwórz
Pokaż pełny widok rekordu Zobacz statystyki


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