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.