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
- DN-1.in, DN-1.proof
- DN-13345.in, DN-13345.proof
- DN-20615.in, DN-20615.proof
- DN-20629.in, DN-20629.proof
- DN-20775.in, DN-20775.proof
- DN-20787.in, DN-20787.proof
- DN-24070.in, DN-24070.proof
- DN-24086.in, DN-24086.proof
- DN-24412.in, DN-24412.proof
- DN-24429.in, DN-24429.proof
- DN-24970.in, DN-24970.proof
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
- open-16 (the 16 open candidates of length 15)
- Update (August 2003): Thomas Hillenbrand has written (by e-mail)
that C_2 and C_5 are, in fact, single axioms.
Waldmeister
proved the theorems, given specialized definitions,
and (for C_5) multiple searches, restarting with lemmas.
- Update (November 2003): A counterexample to C_9 has been found.
6. Automated Deduction Methods
- DN-filter.interps
- DN-search.in, DN-search.proof
- DN-20615.in, DN-20615.proof
(same as above)
- Sh-1-comm.in, Sh-1-comm.proof
- DN-1.in, DN-1.proof
(same as above)
- Sh-1.in, Sh-1.proof
(same as above)
- Sh-2.in, Sh-2.proof
(same as above)
- circle-1.in, circle-1.proof
- circle-2.in, circle-2.proof
- circle-3.in, circle-3.proof
- circle-4.in, circle-4.proof
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.