@ARTICLE{AIMLOOP.MIZ,
  AUTHOR = {Brown, Chad E. and P\k{a}k, Karol},
  NOTE1 = {This work has been supported by the European Research Council (ERC)
       Consolidator grant nr. 649043 \textit{AI4REASON}
       and the Polish National Science Centre granted by decision
       no. DEC-2015/19/D/ST6/01473.
    },
  TITLE = {{AIM} Loops and the {AIM} Conjecture},
  SECTION1 = {Loops -- Introduction},
  SECTION2 = {Multiplicative Mappings and Cosets},
  SECTION3 = {Normal Subloop},
  SECTION4 = {AIM Conjecture},
  DAY = {29},
  MONTH = {August},
  YEAR = {2019},
  ADDRESS1 = {\u{C}esk\'{y} Institut Informatiky Robotiky a Kybernetiky\\
  Zikova 4, 166 36 Praha 6,\\ Czech Republic},
  ADDRESS2 = {Institute of Informatics\\University of Bia{\l}ystok\\ 
  Konstantego Cio{\l}kowskiego 1M, 15-245 Bia{\l}ystok\\Poland},
  SUMMARY = {In this article, we prove, using the Mizar\cite{Role_MML} 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~\ref{sec:2}, we define a set \mbox{Mlt $Q$} of multiplicative 
  mappings of $Q$ and cosets (mostly following Albert 1943 for cosets~\cite{Albert43}).
  Next, in Section~\ref{sec:3} we define the notion of a normal subloop
  and construct quotients by normal subloops.
  In the last section
 we define the set \mbox{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 \mbox{TT}, etc.
  We prove in Theorem~\ref{Th62} that the nucleus of an AIM loop is normal 
  and finally in Theorem~\ref{Th:63} that the AIM Conjecture follows
  from knowing every AIM loop satisfies
 \mbox{aa1}, \mbox{aa2}, \mbox{aa3}, \mbox{Ka}, \mbox{aK1}, \mbox{aK2} and \mbox{aK3}.
  \par The formalization follows M.K. Kinyon, R. Veroff, P. Vojtechovsky \cite{KinyonVV13}
  as well as Veroff's Prover9 files.}
}

@inproceedings{KinyonVV13,
  author    = {Michael K. Kinyon and
               Robert Veroff and
               Petr Vojt{\v{e}}chovsk{\'{y}}},
  title     = {Loops with Abelian Inner Mapping Groups: An Application of Automated
               Deduction},
  booktitle = {Automated Reasoning and Mathematics - Essays in Memory of William
               W. McCune},
  pages     = {151--164},
  year      = {2013},
  crossref  = {2013mccune}
}

@proceedings{2013mccune,
  editor    = {Maria Paola Bonacina and
               Mark E. Stickel},
  title     = {Automated Reasoning and Mathematics - Essays in Memory of William
               W. McCune},
  series    = {Lecture Notes in Computer Science},
  volume    = {7788},
  publisher = {Springer},
  year      = {2013}
}

@ARTICLE{Albert43,
  AUTHOR =       {A. A. Albert},
  TITLE =        {Quasigroups. I},
  JOURNAL =      {Transactions of the American Mathematical Society},
  YEAR =         {1943},
  volume =       {54},
  number =       {3},
  pages =        {507--519},
  publisher =    {American Mathematical Society}
}



