From: Ranganathan Padmanabhan Subject: Re: loops, quasigroups, nonassociative systems Date: Fri, 17 Jun 2005 To: William McCune On Jun 15, 2005, at 9:43 AM, William McCune wrote: > RP, > > I'll be giving an invited talk on July 7 at the Denver conference > on loops, quasigroups, and nonassociative systems. See > > http://www.math.du.edu/milehigh/ > > This talk will be the official release of Prover9. I plan to > give several detailed example problems and proofs, though > I haven't yet decided on the problems. > > Can you suggest some problems that would be of interest to that > audience? I'm looking for easy problems as well has medium > and harder ones, and also counterexample problems for Mace4. Hi Bill, Here is a Problem on quasigroups which might be amenable for treatment by Otter, Mace and Prover9. A Sample Theorem (due to R.P. and Barry Wolk) Let K be the set of all algebras of type (2) satisfying the four identities given below. 1. (x * E) * x = x. 2. x* (x * y) = y. 3. (x * y) * (z * u) = (x * z) * (y * u). 4. ((x * x) * x) * x = ((y * y) * y) * y (=E). Then K satisfies all the identities valid in the ring model (Z[7]; 3x- y). In other words, the variety K has a solvable word problem! Also every model of K is imbeddable in a quasigroup. Solution to the word problem is given like this: An identity f=g is a consequence of {1,2,3,4} if and only if it is true in the ring model mentioned above. Applying MACE and OTTER to prove the above statements. Step#1. MACE. Get a ring model. A non-trivial one must be x*y = 3x - y (mod 7).

mace4 -f ring.in > ring.out ; ### ( ring.out.xml )

Step#2. Use Otter to derive the two cancellation laws. Right cancellation is obvious: x*y = x*z => x*(x*y) = x*(x*z) => y=z by (2). Left cancellation law: x*z = y*z => x=y also follows from the above but not obvious and Otter will love proving this.

prover9 -f cancel1.in > cancel1.out ; ### ( cancel1.out.xml )

prover9 -f cancel2.in > cancel2.out ; ### ( cancel2.out.xml )

Step#3 Prove that E (defined in Id #4) is idempotent.

prover9 -f idempotent.in > idempotent.out ; ### ( idempotent.out.xml )

Human Steps. By a result of M. Sholander, any cancellative medial groupoid with an idempotent element is imbeddable in a medial quasigroup satisfying the same identities of the original algebra. So any algebra belonging to K is a sugroupoid of such a quasigroup. Finally, the classic Toyoda-Bruck theorem asserts that every medial quasigroup is isotopic to an abelian group i.e. a ring model. So x*y = ax + by and plugging in the above four equations, one shows that 3x-y (mod 7) is the only solution for this set of equations. In particular, the identity ((x * y) * z) * u = ((u * y) * z) * x, which is true in the ring model 3x-y (mod 7), must now be an equational consequence of the four identites. This creates new problems for Otter, Prover9. Prove this using Otter or Prover9. Again, two methods. Method I Prove directly {1,2,3,4} ==> ((x * y) * z) * u = ((u * y) * z) * x.

prover9 -f identity.in > identity.out ; ### ( identity.out.xml )

Method II. Prove ((x * y) * z) * u = ((u * y) * z) * x from {1,2,3,4, quasigroup property, skolemize i.e. type (2,2,2) with*,/,\ }.

prover9 -f identity2.in > identity2.out ; ### ( identity2.out.xml )

Obviously Method I is preferable. Thus we have a very good example of a theorem differentiating the "simplicity-and-elegance" of a human proof compared to the "complexity-in-details" of a first order proof. Also, there is no immediate first order human proof of {1,2,3,4} ==> ((x * y) * z) * u = ((u * y) * z) * x. But theorem-provers can do this. Conjecture: This variety defined by the four identities above is one- based. If true, only machines can do this (using, of course, human designed equational filters to eliminate "bad" guys). Other (relatively easy) Problems: Prove that x*(y*(y*x)) = y*x implies y*(y*x) = x*y in quasigroups

prover9 -f qg1.in > qg1.out ; ### ( qg1.out.xml )

but not in cancellative groupoids.

prover9 -t 10 -f qg2.in > qg2.out ; ### ( qg2.out.xml )

(Mace4 cannot help, because it looks for finite models only.)

Prove that (xy)(zu) = (xz)(yu) implies (x(yz))((uv)w) = (x(uz))((yv)w) in cancellation groupoids with an idempotent or under (gL) but not in general. (Prover9, Otter with gL), Mace).

prover9 -f cg1.in > cg1.out ; ### ( cg1.out.xml )

Good luck with your conference. R. P.