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.
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.outprooftrans -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").
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.
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.
(x * y) * (y \ 1) = x # label("RIP").
(x \ 1) * (y \ 1) = (x * y) \ 1 # label("AIP").
% Left inner maps preserve inverses L(x,y,z) \ 1 = L(x \ 1,y,z) # label("LIMPI").
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").
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.