English

Loops with abelian inner mapping groups: An application of automated deduction

Group Theory 2015-09-21 v1

Abstract

We describe a large-scale project in applied automated deduction concerned with the following problem of considerable interest in loop theory: If QQ is a loop with commuting inner mappings, does it follow that QQ modulo its center is a group and QQ modulo its nucleus is an abelian group? This problem has been answered affirmatively in several varieties of loops. The solution usually involves sophisticated techniques of automated deduction, and the resulting derivations are very long, often with no higher-level human proofs available.

Keywords

Cite

@article{arxiv.1509.05468,
  title  = {Loops with abelian inner mapping groups: An application of automated deduction},
  author = {Michael Kinyon and Robert Veroff and Petr Vojtěchovský},
  journal= {arXiv preprint arXiv:1509.05468},
  year   = {2015}
}