Publications

R. Veroff and W. McCune, "A Short Sheffer Axiom for Boolean Algebra," Technical Memorandum ANL/MCS-TM-244, June 2000. [pdf]

A short Sheffer stroke identity is shown to be a single axiom for Boolean algebra. The axiom has length 15 and 3 variables. The proof shows that it is equivalent to Sheffer's original 3-basis for the theory. Automated deduction techniques were used to find the proof. The shortest single axiom previously known to us has length 105 and 6 variables.