Loops with Abelian Inner Mapping Groups:
an Application of Automated Deduction
(Web Support)

Michael Kinyon, Bob Veroff and Petr Vojtechovsky

March 2012

This page provides Web support for Loops with Abelian Inner Mapping Groups and Automated Deduction [3]. In particular, we present a proof of the main result of the paper (for LC loops) that was found with the assistance of the program Prover9 [1]. For illustration, we also present a few of the intermediate results that served as proof sketches [2] for the LC-loop result.

Paper 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.

Prover9 Proofs

In all cases, the objective is to show that the 7 goals, 
   a(K(x,y),z,u) = 1    # label("aK1").
   a(x,K(y,z),u) = 1    # label("aK2").
   a(x,y,K(z,u)) = 1    # label("aK3").

   K(a(x,y,z),u) = 1    # label("Ka").

   a(a(x,y,z),u,w) = 1  # label("aa1").
   a(x,a(y,z,u),w) = 1  # label("aa2").
   a(x,y,a(z,u,w)) = 1  # label("aa3").
follow from the AIM axioms plus axioms included as a special case of interest or as temporary extra assumptions for an intermediate result.

For each proof, we include input, output, proof and xml files created as follows.

prover9 -f file.in > file.out

prooftrans -f file.out > file.pf

prooftrans xml -f file.out > file.xml

The first proof is for an intermediate result that includes the Moufang Loop axiom M1 as an extra assumption. We note that intermediate results may or may not be of interest on their own; in this case, we had already proved as part of the larger AIM project that M1 suffices by itself. The primary purpose here is to find proof sketches that provide guidance for future searches.

Theorem. {AIM, Moufang (M1), LC} => all 7 goals. 

   ... AIM axioms ...
   (x * y) * x) * z = x * (y * (x * z)) # label("Moufang (M1)").
   (x * (x * y)) * z = x * (x * (y * z)) # label("LC").

Proof. (in, out, pf, xml)

Note that this proof is found without using any input hints for guidance. It provides a first proof sketch, showing steps that suffice for proving the 7 goals of interest.

The second proof is a strictly-forward and demodulation-free derivation of the same theorem. In our experience, these make better proof sketches for future searches. Here we use the first proof as hints to help us find this proof. The hints are extracted using the Prooftrans utility (from the Prover9 distribution) with the "expand hints" option.

Proof. (in, out, pf, xml)

There were several more intermediate results providing proof sketches that ultimately led to the proof of the LC-loop result. Here are a few examples.

Finally, we get to the main result of the paper.

Theorem. {AIM, LC} => all 7 goals. 

   ... AIM axioms ...
   (x * (x * y)) * z = x * (x * (y * z)) # label("LC").

Proof. (in, out, pf, xml)

This essentially is a proof checking run. At this point, we've already proved the theorem, relying on a substantial set of hints from multiple proof sketches. We run Prover9 one more time with just the most recent proof included as hints.

References

  1. W. McCune. Prover9. http://www.cs.unm.edu/~mccune/prover9.
  2. R. Veroff. Solving open questions and other challenge problems using proof sketches. Journal of Automated Reasoning, 27(2):157-174, 2001. (postscript)
  3. M. Kinyon, P. Vojtechovsky and R. Veroff. Loops with abelian inner mapping groups: an application of automated deduction. Submitted for publication.