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

TL;DR

This paper explores the use of automated deduction techniques to analyze loops with abelian inner mapping groups, aiming to determine structural properties related to their centers and nuclei.

Contribution

It applies large-scale automated deduction to a complex problem in loop theory, providing insights into the structure of loops with commuting inner mappings.

Findings

Automated deduction successfully analyzed complex loop structures.

Long derivations were obtained without higher-level human proofs.

The approach advances understanding of loop properties with abelian inner mappings.

Abstract

We describe a large-scale project in applied automated deduction concerned with the following problem of considerable interest in loop theory: If $Q$ is a loop with commuting inner mappings, does it follow that $Q$ modulo its center is a group and $Q$ 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.