Short Single Axioms for Boolean Algebra

William McCune, Robert Veroff, Branden Fitelson, Kenneth Harris, Andrew Feist, Larry Wos

June 2000 (Revised December 2002)


This web page contains material in support of a paper of the same name in the Journal of Automated Reasoning 29 (1), pages 1--16, 2002. Here is a preprint of the paper.
Here are the links that correspond to the "pseudo-links" in the paper.

1. Background and Introduction

2. A Basis for Disjunction and Negation

3. A Basis for the Sheffer Stroke

4. (Sh_1) is a Shortest 1-Basis for the Sheffer Stroke

5. An Exhaustive List of Possible 15-Symbol Single Axioms

6. Automated Deduction Methods

7. Summary and Questions


Additional Material

In a footnote on the third page of the paper we write:
Wolfram's 25 candidates are precisely the set of Sheffer identities of length <= 15 (excluding mirror images) that have no noncommutative models of size <=4.
Here is how one can use MACE 2.0 to derive the 25 candidates.