\documentclass{au} \usepackage{amssymb,latexsym} \usepackage{float} %% so that we can put tables HERE!!! \begin{table}[H] % Join, Meet, and Sheffer Stroke symbols (to be used in math mode) % \newcommand{\J}{\vee} % \newcommand{\M}{\wedge} \newcommand{\M}{\negthinspace\wedge\negthinspace} \newcommand{\J}{\negthinspace\vee\negthinspace} \renewcommand{\SS}{\ |\ } % The varieties (to be used when referring to the set of algebras) \newcommand{\LT}{$\mathcal{L}$} \newcommand{\OL}{$\mathcal{OL}$} \newcommand{\OML}{$\mathcal{OML}$} \newcommand{\MOL}{$\mathcal{MOL}$} \newcommand{\BA}{$\mathcal{BA}$} \begin{document} % \sloppy \title{Automated Discovery of Single Axioms for Ortholattices} \author{W. McCune} \address{W. McCune\footnote{Supported by the Mathematical, Information, and Computational Sciences Division subprogram of the Office of Advanced Scientific Computing Research, Office of Science, U.S. Department of Energy, under Contract W-31-109-ENG-38.}\\ Mathematics and Computer Science Division\\ Argonne National Laboratory\\ Argonne, IL 60439, USA} \email{mccune@mcs.anl.gov} % \urladdr{http://www.mcs.anl.gov/\~{}mccune} \author{R. Padmanabhan} \address{R. Padmanabhan\footnote{Supported by an operating grant from NSERC of Canada, grant \#8215-02.}\\ Department of Mathematics\\ University of Manitoba\\ Winnipeg R3T 2N2, CANADA} \email{padman@cc.umanitoba.ca} \author{M. A. Rose} \address{M. A. Rose\footnote{Supported by the Division of Educational Programs, Argonne National Laboratory.}\\ Department of Mathematics\\ University of Wisconsin-Madison\\ Madison, WI 53706, USA} \email{rose@math.wisc.edu} \author{R. Veroff} \address{R. Veroff\footnote{Supported by National Science Foundation grant CDA-9503064.}\\ Department of Computer Science\\ University of New Mexico\\ Albuquerque, New Mexico 87131\\ U.S.A.} \email{veroff@cs.unm.edu} % \urladdr{http://www.cs.unm.edu/\~{}veroff} \keywords{ortholattice basis, ortholattice single identity} \subjclass{Primary: 03G10; Secondary: 06B99} \date{February 23, 2004} \begin{abstract} We present short single axioms for ortholattices, orthomodular lattices, and modular ortholattices, all in terms of the Sheffer stroke. The ortholattice axiom is the shortest possible. We also give multiequation bases in terms of the Sheffer stroke and in terms of join, meet, and complementation. Proofs are omitted but are available in an associated technical report and on the Web. We used computers extensively to find candidates, reject candidates, and search for proofs that candidates are single axioms. \end{abstract} \maketitle \section{Introduction} \label{sec-intro} Consider the problem of expressing equational theories as simply as possible---with the least number of symbols, the least number of equations, the least number of operations, and the least number of variables. The problem for Abelian groups was solved by Tarski in 1938 \cite{tarski-abelian-sax} with the single axiom $ x / (y / (z / (x / y))) = z$ in terms of the division operation. Other varieties of groups (including other operations) have been addressed, and short single axioms have been found, but minimality has not been proved in most cases. The problem for Boolean algebra was solved recently with a shortest single axiom in terms of the Sheffer stroke operation \cite{basax-jar}. Progress has recently been made also for lattices, with a reasonably short single axiom in terms of join and meet \cite{ltsax-au}. In this paper we consider a chain of varieties between the lattices and the Boolean algebras, namely, ortholattices, orthomodular lattices, and modular ortholattices. The main results of the work we report here are all in terms of the Sheffer stroke---a shortest single axiom for ortholattices, and short single axioms for orthomodular lattices and modular ortholattices. We also include multiequation bases for these varieties. We used several computer programs in this work. Otter \cite{otter33} searches for proofs, Mace \cite{mace4} searches for models and counterexamples, and other programs embody decision and enumeration procedures. We claim, throughout the paper, that Otter proves theorems and that Mace finds counterexamples. We have omitted the proofs and counterexamples because they are long and because they do not seem to give insight into the mathematics. The proofs and counterexamples can be found in a technical report \cite{olsax-tm} and on a Web page \cite{olsax-web}. The Web page contains, in addition, input and output files for Otter and Mace and demonstrations of the enumeration, decision, and filtering programs that were used. \section{Multiequation Bases} \label{sec-bases} We define the relevant varieties first in terms of join, meet, and complementation and then in terms of the Sheffer stroke. \subsection{In Terms of Join/Meet/Complementation} Consider the following equations. \begin{equation*} \begin{array}{ll} \text{AJ:} & x \J (y \J z) = y \J (x \J z) \\ \text{AM:} & x \M (y \M z) = y \M (x \M z) \\ \text{B1:} & x \J (x \M y) = x \\ \text{B2:} & x \M (x \J y) = x \\ \text{DM:} & x \M y = (x' \J y')' \\ \text{CC:} & x'' = x \\ \text{ONE:} & x \J x' = y \J y' \\ \text{OM:} & x \J (x' \M (x \J y)) = x \J y \\ \text{MOD:} & x \J (y \M (x \J z)) = x \J (z \M (x \J y)) \\ \text{CUT:} & (x \J y') \M (x \J y) = x \end{array} \end{equation*} The lattices (\LT), ortholattices (\OL), orthomodular lattices (\OML), modular ortholattices (\MOL), and Boolean algebras (\BA) can be defined as shown in the following table. \begin{center} \begin{tabular}{lll} Variety & Type & Basis \\ \hline \LT & $\langle 2,2 \rangle$ & \{ AJ, B1, AM, B2 \} \\ \OL & $\langle 2,2,1 \rangle$ & \{ AJ, B1, DM, CC, ONE \} \\ \OML & $\langle 2,2,1 \rangle$ & \{ AJ, B1, DM, OM \} \\ \MOL & $\langle 2,2,1 \rangle$ & \{ AJ, B1, DM, CC, ONE, MOD \} \\ \BA & $\langle 2,2,1 \rangle$ & \{ AJ, DM, ONE, CUT \} \end{tabular} \end{center} Otter can easily prove that these bases are equivalent to other bases given in the literature (for example, by deriving the commutativity laws from the \LT\ basis), Mace can easily show that all but the \BA\ basis are independent (we do not know if ONE is necessary), Otter can easily show that these varieties form the chain \begin{equation*} \text{\LT} \supset \text{\OL} \supset \text{\OML} \supset \text{\MOL} \supset \text{\BA}, \end{equation*} and Mace can easily show that those inclusions are proper. \subsection{In Terms of the Sheffer Stroke} \newcommand{\Ass}{$\widehat{\text{A}}$} \newcommand{\Bss}{$\widehat{\text{B}}$} \newcommand{\ONEss}{$\widehat{\text{ONE}}$} \newcommand{\OMss}{$\widehat{\text{OM}}$} \newcommand{\MODss}{$\widehat{\text{MOD}}$} \newcommand{\CUTss}{$\widehat{\text{CUT}}$} The lattices cannot be defined in terms of a single binary operation \cite{gratzer:1998}, but \OL\ and its subvarieties can be, in particular, in terms of the Sheffer stroke ``$|$''. \begin{center} \begin{tabular}{ll} $|$ in terms of $\J,\M,'$\ \ \ & $\J,\M,'$ in terms of $|$ \\ \hline $x|y = x' \J y'$ & $x \J y = (x|x)|(y|y)$ \\ & $x \M y = (x|y)|(x|y)$ \\ & $x' = x|x$ \end{tabular} \end{center} Rewriting a basis to a different set of operations does not necessarily produce a basis in terms of that other set of operations. If we use the definitions just given to rewrite a Sheffer stroke basis in terms of join and complementation, we do not get a basis in terms of join and complementation. This statement applies to \OL, \OML, \MOL, and \BA, and it is independent of the basis we start with. Consider (BA2), a single axiom for \BA\ \cite{basax-jar}. Construct candidate (BA2$'$) from (BA2) by replacing $x \SS y$ with $x' \J y'$ throughout as follows (the spacing shows the correspondence). \begin{verbatim} (y | ((x | y ) | y ) ) | (x | (z | y ) ) = x (BA2) (y' v ((x' v y')' v y')')' v (x' v (z' v y')')' = x (BA2') \end{verbatim} If (BA2') were a single axiom, we would be able to derive associativity of join, but this is impossible: if we interpret $x'$ as $x$, (BA2') becomes identical to (BA2) except for the operation symbol; hence the models of (BA2), in which the Sheffer stroke is nonassociative, immediately give models of (BA2') in which join is nonassociative. Considering the other direction, if we rewrite a join/meet/complementation basis in terms of the Sheffer stroke, we do obtain a basis in terms of the Sheffer stroke (the proof is omitted). However, this translation can produce equations more complicated than necessary; for example, equation AJ rewritten to the Sheffer stroke is \begin{equation*} (x|x)|(((y|y)|(z|z))|((y|y)|(z|z))) = (y|y)|(((x|x)|(z|z))|((x|x)|(z|z))). \end{equation*} However, because the Sheffer stroke operation builds in properties of complementation, we can find simpler bases with Sheffer stroke than with join, meet, and complementation. Consider the following equations. \begin{equation*} \begin{array}{ll} \text{\Ass:} & x \SS ((y \SS z) \SS (y \SS z)) = y \SS ((x \SS z) \SS (x \SS z)) \\ \text{\Bss:} & (x \SS x) \SS (x \SS y) = x \\ \text{\ONEss:} & x \SS (x \SS x) = y \SS (y \SS y) \\ \text{\OMss:} & x \SS (x \SS (x \SS y)) = x \SS y \\ \text{\MODss:} & x \SS (y \SS (x \SS (z \SS z))) = x \SS (z \SS (x \SS (y \SS y))) \\ \text{\CUTss:} & (x \SS (y \SS y)) \SS (x \SS y) = x \end{array} \end{equation*} The varieties in question can be defined as shown in the following table. \begin{center} \begin{tabular}{lcl} Variety & Type & Basis \\ \hline \OL & $\langle 2 \rangle$ & \{ \Ass, \Bss, \ONEss\ \} \\ \OML & $\langle 2 \rangle$ & \{ \Ass, \Bss, \OMss\ \} \\ \MOL & $\langle 2 \rangle$ & \{ \Ass, \Bss, \ONEss, \MODss\ \} \\ \BA & $\langle 2 \rangle$ & \{ \Ass, \CUTss\ \} \end{tabular} \end{center} Mace easily shows that these bases are independent, and Otter easily proves that these bases are definitionally equivalent to the join/meet/complementation bases in the preceding subsection. \subsection{Do Simpler Multiequation Bases Exist?} Our goal in producing the multiequation bases was to find short, intuitive, and fairly standard bases in terms of join/meet/complementation and then to find similar bases in terms of the Sheffer stroke. We doubt that the preceding bases are the shortest. In fact, for \BA\ in terms of the Sheffer stroke, the 2-basis with the least number of symbols is known to be \{~$x \SS y = y \SS x$, $(x \SS y) \SS (x \SS (y \SS z)) = x$~\} \cite{veroff-sheffer}. For \BA\ in terms of the join and complementation, the simplest 2-basis we know of is \{~$(x' \J y)' \J x = x$, $(x' \J y)' \J (z \J y) = y \J (z \J x)$~\} \cite{meredith-eq}. \section{Single Axioms} \label{sec-sax} It is well known that any finitely-based variety of \OML\ is one-based \cite{rp-quack:congruences}. This is a consequence of the existence of Gould-Gr\"atzer-Pixley (GGP) terms \cite{gould-gratzer,pixley} in these varieties; that is, terms $g(x,y,z)$ such that $g(y,y,x)=g(x,z,z)=g(x,u,x) = x$. For example, $(x \M z) \J ((y \M z)' \M z) \J ((x \M y)' \M x)$ is a GGP term for \OML. The variety \OL\ does not admit GGP terms, and existence of single axioms is known by a different result \cite{rp-major}, relying on a basis consisting entirely of absorption equations and the presence of majority terms; that is, terms $m(x,y,z)$ such that $m(x,x,y)=m(x,z,x)=m(u,x,x) = x$. By those results, there exist procedures to construct single axioms for these varieties, but the basic procedures have exponential behavior, producing very large axioms, sometimes with millions of symbols. The procedures can be optimized somewhat \cite{wwm-rp:lt-wal}, but they still tend to produce axioms with hundreds of symbols. Our approach is to start small, considering all possible candidate equations of a given size, and looking at sizes as large as practical. If all goes well, we can show that a candidate is a shortest single axiom by proving a known basis and by eliminating all shorter candidates. In other cases, we can find single axioms without being able to eliminate all shorter candidates. A similar approach led, in previous work, to axiom LT1 (below) for lattice theory \cite{ltsax-au}, axiom BA1 for Boolean algebra \cite{basax-jar}, and BA2, which is a shortest axiom for Boolean algebra in terms of the Sheffer stroke \cite{basax-jar}. \begin{equation*} \begin{array}{ll} \text{LT1:} & (((y \J x) \M x) \J (((z \M (x \J x)) \J (u \M x)) \M v)) \M (w \J ((s \J x) \M (x \J t))) = x\\ \text{BA1:} & ((y \J z)' \J x')' \J ((u' \J u)' \J (x' \J y))' = x\\ \text{BA2:} & (y \SS ((x \SS y) \SS y)) \SS (x \SS (z \SS y)) = x \end{array} \end{equation*} Our goal in this work was to find short single axioms for \OL, \OML, and \MOL\ in terms of the Sheffer stroke. \subsection{Generating and Filtering Candidates} The procedure to generate candidates equations is roughly as follows. \begin{itemize} \item Generate all well-formed Sheffer stroke equations of a given length satisfying the following constraints: (1) it has at least three variables; (2) its right-hand side is a variable, say $x$; (3) neither the leftmost nor the rightmost variable of the left-hand side is $x$; (4) it cannot be of the form $y | \alpha =x$ or $\alpha | y=x$ for any variable $y$; and (5) if it is $\alpha | \beta = x$, then length($\alpha$) $\leq$ length($\beta$). Justifications for these constraints can be found in \cite{basax-jar}. \item Pass the equations through a decision procedure for Boolean algebra identities. A vast majority of the equations are removed by this check. \item Remove equations that are not valid in the variety in question. For \OL\ we have a decision procedure for this. For \OML\ and \MOL, for which there is no decision procedure \cite[p. 218]{kalmbach}, we can test the equations against a set of finite models of the variety (perhaps admitting some nonidentities). \item Eliminate candidates that are too weak to be single axioms. We do not have a perfect test for this. In practice, we iteratively collect sets of nonmodels by using the program Mace. Consider \OL. If a candidate is false in all of the current non-\OL s, we use Mace to look for non-\OL\ models of the candidate. If one is found, we add it to the set and eliminate the candidate. We call this process \emph{filtering the candidates}, and we refer to the nonmodels as \emph{filters}. \end{itemize} Let the \emph{length} of a term or equation be the number of occurrences of variables and operators (including the equal sign but not parentheses). For example, $(x \SS x) \SS (x \SS y) = x$ has length 9. Note that Sheffer stroke equations have odd length. In the \OL\ case, all candidates up through length 21 can be eliminated by a set of four non-\OL s \cite[file non-OL.A-4]{olsax-web} of sizes 3, 6, 6, and 8. A single axiom (OL-Sh below) was found among the candidates of length 23. In the \OML\ case, all candidates up through length 19 can be eliminated with a set of nine non-\OL s \cite[file non-OL.B-9]{olsax-web}, all of size $\leq 6$. For length 21, we could not eliminate all candidates, and we could not prove any of the survivors to be single axioms. A set of 23 non-\OL s was accumulated \cite[file non-OL.C-23]{olsax-web}, eliminating all but 58 candidates. A single axiom (OML-Sh below) was found among the candidates of length 23. The \MOL\ case started out like the \OML\ case, with the elimination of all candidates up through length 19 by using the same filters as in the \OML\ case. For length 21, 14 more non-\OL s were accumulated \cite[file non-OL.D-14]{olsax-web}, and the nine nonmodular \OML s up through size 16 were also used as filters. However, 238 length 21 candidates survived, and none was proved to be a single axiom. As the candidates grow, it becomes more difficult to find counterexamples, so we used the existing non-\MOL s to filter candidates of lengths 23, 25, and 27. A single axiom (MOL-Sh below) was found among those of length 25. \subsection{An Example Candidate and Counterexample} One of the \OML\ candidates was the identity \begin{equation} ((x \SS y) \SS y) \SS (((z \SS y) \SS (x \SS y)) \SS ((x \SS x) \SS z)) = y. \tag{C} \end{equation} Given this candidate, with no additional constraints, Mace could not find a counterexample in a reasonable amount of time. However, when asked Mace to search for a quasigroup model of (C), it immediately found the following structure. % \begin{table}[H] \centering % size 7 \begin{center} \begin{tabular}{r|rrrrrrr} & 0 & 1 & 2 & 3 & 4 & 5 & 6\\ \hline 0 & 0 & 2 & 1 & 4 & 3 & 6 & 5 \\ 1 & 3 & 5 & 4 & 0 & 2 & 1 & 6 \\ 2 & 4 & 3 & 6 & 1 & 0 & 5 & 2 \\ 3 & 5 & 1 & 3 & 2 & 6 & 0 & 4 \\ 4 & 6 & 4 & 2 & 5 & 1 & 3 & 0 \\ 5 & 2 & 6 & 0 & 3 & 5 & 4 & 1 \\ 6 & 1 & 0 & 5 & 6 & 4 & 2 & 3 \end{tabular} \end{center} % \caption{Structure 19 of non-OL.C-23} % \end{table} It is easy to see that this structure is not an ortholattice with respect to the Sheffer stroke (e.g., because it contains an idempotent element, or because it is noncommutative, or simply because it is a quasigroup). Hence, (C) cannot be a single axiom for any subvariety of \OL. This structure became a member of the filter set non-OL.C-23 listed in \cite{olsax-web}. \subsection{Trying to Prove That Candidates Are Single Axioms} Given a set of candidates that had survived all the filters, we tried to prove each to be a single axiom by deriving a known basis, for example, the independent bases given in Section~\ref{sec-bases}. Automatic proofs were attempted with hundreds of \OL\ candidates, thousands of \OML\ candidates, and hundreds of thousands of \MOL\ candidates before proofs were found for the three cases. The time allocated for each candidate varied from a few minutes to a few seconds, depending on the size of the set. For each proof attempt, we included as goals several important properties of the variety as well as a known basis. If some interesting properties were derived from the candidate, but not enough for a complete proof, we investigated that candidate later with focused proof attempts. Length 23 single axioms for \OL\ and \OML\ were found without much difficulty. The proofs were not trivial for Otter, but they were found automatically within a few minutes. Finding a \MOL\ axiom was much more difficult. Many more candidates had to be considered, and proofs with the successful candidates were not found automatically. Promising candidates (those that proved the most interesting properties) were selected from the automatic attempts, and advanced automated deduction techniques involving human guidance (i.e., the method of hints and sketches \cite{veroff:sketches}) were applied, producing a proof for one candidate of length 25. \subsection{Single Axioms for \OL, \OML, and \MOL} We give here the main results of the project---single axioms, in terms of the Sheffer stroke, for \OL, \OML, and \MOL. Proofs can be found in \cite{olsax-tm} and in \cite{olsax-web}. For completeness, we also list (BA2), a shortest single axiom for \BA\ \cite{basax-jar}. \begin{equation*} \begin{array}{ll} \text{OL-Sh:} & (((y\SS x)\SS (x\SS z))\SS u)\SS (x\SS ((x\SS ((y\SS y)\SS y))\SS z))=x\\ \text{OML-Sh:} & (((y\SS x)\SS (x\SS z))\SS u)\SS (x\SS ((z\SS ((x\SS x)\SS z))\SS z))=x\\ \text{MOL-Sh:} & (y\SS x)\SS (((x\SS x)\SS z)\SS (((((x\SS y)\SS z)\SS z)\SS x)\SS (x\SS u)))=x\\ \text{BA2:} & (y \SS ((x \SS y) \SS y)) \SS (x \SS (z \SS y)) = x \end{array} \end{equation*} The \OL\ axiom (length 23) is the shortest possible. We do not know whether the \OML\ axiom (length 23) or the \MOL\ axiom (length 25) are shortest. With the exception of (BA2), each of these axioms has four variables, and the question of short 3-variable axioms is open. In the \OL\ case, all of the surviving length-23 candidates have 4 variables, so any 3-variable \OL\ axioms must have length $\geq 25$. In the \OML\ case, four of the 58 length-21 and many of the length-23 candidates have three variables. In the \MOL\ case, many of the surviving candidates of lengths 21 and 23 have three variables. \section{Conclusion} Symbolic computation was used in five ways in this work: (1) to enumerate equations subject to a set of syntactic constraints, (2) to evaluate equations with respect to finite structures, (3) to decide ortholattice identities, (4) to search (with Otter) for equational proofs, and (5) to search (with Mace) for finite algebras that satisfy sets of equations and disequations. The first three ways are relatively straightforward, although the programs were coded efficiently so that they could handle billions of equations. Otter and Mace are available for download from the Web page associated with this paper \cite{olsax-web}. The proofs in this work fall into several classes: proofs by equational deduction, independence proofs by finite counterexamples, and minimality proofs by exhaustive enumeration. The minimality proofs are fundamentally different from the Otter or Mace proofs and are similar in spirit (though not in scale or interest) to proofs of the four-color theorem. In short, the problem is reduced to a finite set of cases that are checked by computers. Soundness is especially questionable, with reliance (in our case) on optimized special-purpose code for the equation generation and decision procedures. We doubt that much can be learned from the various components of the minimality proofs. The Otter proofs and Mace counterexamples, on the other hand, are creative in the sense that we had no idea what the proofs or structures might be and the proofs, with the exception of the \MOL\ single axiom proof, required little human guidance. \bibliographystyle{plain} % \bibliography{/home/mccune/papers/bib/master} \begin{thebibliography}{10} \bibitem{gould-gratzer} M.~I. Gould and G.~{Gr\"atzer}. \newblock Boolean extensions and normal subdirect powers of finite universal algebras. \newblock {\em Math. Zeitschr.}, 99:16--25, 1967. \bibitem{gratzer:1998} G.~{Gr\"atzer}. \newblock {\em General Lattice Theory}. \newblock Birkhauser Verlag, 2nd edition, 1998. \bibitem{kalmbach} G.~Kalmbach. \newblock {\em Orthomodular Lattices}. \newblock Academic Press, New York, 1983. \bibitem{mace4} W.~McCune. \newblock Mace4 {R}eference {M}anual and {G}uide. \newblock Tech. Memo ANL/MCS-TM-264, Mathematics and Computer Science Division, Argonne National Laboratory, Argonne, IL, August 2003. \bibitem{otter33} W.~McCune. \newblock Otter 3.3 {R}eference {M}anual. \newblock Tech. Memo ANL/MCS-TM-263, Mathematics and Computer Science Division, Argonne National Laboratory, Argonne, IL, August 2003. \bibitem{wwm-rp:lt-wal} W.~McCune and R.~Padmanabhan. \newblock Single identities for lattice theory and for weakly associative lattices. \newblock {\em Algebra Universalis}, 36(4):436--449, 1996. \bibitem{olsax-tm} W.~McCune, R.~Padmanabhan, M.~A. Rose, and R.~Veroff. \newblock Short equational bases for ortholattices: Proofs and countermodels. \newblock Tech. Memo ANL/MCS-TM-265, Mathematics and Computer Science Division, Argonne National Laboratory, Argonne, IL, September 2003. \bibitem{olsax-web} W.~McCune, R.~Padmanabhan, M.~A. Rose, and R.~Veroff. \newblock Short equational bases for ortholattices: Web support. \newblock \verb|http://www.mcs.anl.gov/~mccune/papers/olsax/|, 2003. \bibitem{ltsax-au} W.~McCune, R.~Padmanabhan, and R.~Veroff. \newblock Yet another single law for lattices. \newblock {\em Algebra Universalis}. \newblock To appear. \bibitem{basax-jar} W.~McCune, R.~Veroff, B.~Fitelson, K.~Harris, A.~Feist, and L.~Wos. \newblock Short single axioms for {B}oolean algebra. \newblock {\em J. Automated Reasoning}, 29(1):1--16, 2002. \bibitem{meredith-eq} C.~A. Meredith and A.~N. Prior. \newblock Equational logic. \newblock {\em Notre Dame J. Formal Logic}, 9:212--226, 1968. \bibitem{rp-major} R.~Padmanabhan. \newblock Equational theory of algebras with a majority polynomial. \newblock {\em Algebra Universalis}, 7(2):273--275, 1977. \bibitem{rp-quack:congruences} R.~Padmanabhan and R.~W. Quackenbush. \newblock Equational theories of algebras with distributive congruences. \newblock {\em Proc. AMS}, 41(2):373--377, 1973. \bibitem{pixley} A.~F. Pixley. \newblock The ternary discriminator function in universal algebra. \newblock {\em Math. Ann.}, 191:167--180, 1971. \bibitem{tarski-abelian-sax} A.~Tarski. \newblock Ein {B}eitrag zur {A}xiomatik der {A}belschen {G}ruppen. \newblock {\em Fundamenta Mathematicae}, 30:253--256, 1938. \bibitem{veroff:sketches} R.~Veroff. \newblock Solving open questions and other challenge problems using proof sketches. \newblock {\em J. Automated Reasoning}, 27(2):157--174, 2001. \bibitem{veroff-sheffer} R.~Veroff. \newblock A shortest 2-basis for {B}oolean algebra in terms of the {S}heffer stroke. \newblock {\em J. Automated Reasoning}, 31(1):1--9, 2003. \end{thebibliography} \end{document}