\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}
