Product and Inverse

Generating Candidates

(Not written yet.)

The method not very interesting. The result is the 20,568 product/inverse candidates of size (18,3) satisfying the basic constraints.

Finding the Counterexamples

This section contains a (cleaned-up) account of how the countermodels were found. In particular, it doesn't show the jobs that failed to find countermodels.

We used a Perl script called attack, which collects a set of countermodels and filters candidates w.r.t. those countermodels. Attack takes two filename as arguments, reads a stream of candidates from the standard input, and writes filtered candidates to the standard ouput. For example,

    attack head interps < candidates > candidates.filtered

The file "head" is a Mace4 input file, and "interps" (which must not exist when attack is called) is the set of structures that is constructed during execution of the command.

We have 20,568 candidates in cand0, and we start attacking.

    attack head.2-3  interps.2-3   < cand0 > cand1  
 
    attack head.r9   interps.r9    < cand1 > cand2 
 
    attack head.r29  interps.r29   < cand2 > cand3 
 
    attack head.da10 interps.da10  < cand3 > cand5

Next we ran a simple Mace4 job, without a candidate, to get all nonassociative diassociative inverse loops (is that what they're called??) of size 12. We get 16 of them; we could run isofilter to get rid of the isomorphic ones (leaving 2), but that takes a half an hour and is not necessary here.

    mace4 -n12 -m -1 < da.in | get_interps > interps.da12 
 
    modfilter interps.da12 false_in_all < cand5 > cand6 
 
    attack head.r41 interps.r41    < cand6 > cand7

Then we ran some Otter jobs on the candidates. One of them seemed close to being a single axiom, deriving all but associativity, so we ran some Mace4 jobs, including a lot of group-like properties that were derived. A size-16 countermodel was found, which eliminated that candidate and 5 others.

    mace4 < da16.in | get_interps > interps.da16 
 
    modfilter interps.da16 false_in_all < cand7 > cand8

Thirty-six candidates remain. (Some of those can be derived from others, and others can be completed, showing they are not single axioms.)

Update, May 2007

In the Spring of 2007, Michael Kinyon joined the project and made several important contributions.

Six more candidates were eliminated, four of the remaining candidates were shown to be equivalent, and several insights arose.

Kinyon's email summary.

From the 36 candidates, if we remove the four that complete*, the six with finite counterexamples, and three that are redundant because they are equivalent to another, we are left with 23 candidates.

*By "complete", we mean that if we apply Knuth-Bendix completion to the candidate, the procedure terminates without deriving enough to be a basis for group theory. This shows that the candidate is not a single axiom, but it does not produce an explicit counterexample.