January 2014 (Updated February 2016)

This is an addendum to the work presented in www.cs.unm.edu/~veroff/BA/. In particular, we now (January 2014) have a Prover9 proof that Candidate C2,

   f(f(y, f(y, f(x, y))), f(x, f(z, y))) = x # label("Candidate C2").

from the paper

Short Single Axioms for Boolean Algebra
W. McCune, R. Veroff, B. Fitelson, K. Harris, A. Feist and L. Wos
Journal of Automated Reasoning 29(1):1-16, 2002.

is a single axiom for Boolean algebra in terms of the Sheffer Stroke. We believe that this result was already shown in 2003 using Waldmeister, but we have not seen that proof and don't know the details of how that proof was found.

See www.cs.unm.edu/~veroff/BA/ for a discussion of the original problem and this cross reference between the original candidate list and the candidate equations appearing in our JAR paper. Note that Candidate C2 is Equation 4 from the original list of 25 candidate equations.

The Prover9 proof makes use of the defined functions C() and D(),

   C(x) = f(x, f(x, x))
   D(x) = f(f(x, x), x)

and derives the known system

    f(x, y) = f(y, x)             # label("Commutativity").
    f(f(x, y), f(x, f(y, z))) = x # label("Equation 26a").

Here are links to the relevant input, output, proof and xml files: (in, out, pf, xml)

We note that this essentially is a proof checking run, since it includes as hints the steps from a proof found in a less constrained Prover9 search.