### MACE4 Example: Sheffer BA Candidates

This directory contains an example of a Perl program that
runs s sequence of MACE4 jobs.
The file
Sheffer-mgi-without-mirrors
contains 352 Boolean algebra identities in terms of the Sheffer stroke.
Every such identity of length up through 15, or its mirror image,
is subsumed by a member of that file.

The Perl program
commute4_filter
goes through a file of
equations (one equation per line) and calls MACE4 for each,
looking for a noncommutative model of size up through 4.
If none exists, the equation is printed.

The command

commute4_filter < Sheffer-mgi-without-mirrors > candidates

should produce 25 candidates in a few seconds.
This process eliminates candidates that are too weak to be single
axioms for Boolean Algebra in terms of the Sheffer Stroke, because
they have noncommutative models.

NOTE: You might have to edit commute4_filter to point it at the MACE4 binary.

*
These activities are projects of the
Mathematics and Computer Science Division
of
Argonne National Laboratory.
*