\documentstyle[epsf,11pt]{article}

\setlength{\textwidth}{5.5in}
\setlength{\textheight}{9in}
\setlength{\hoffset}{-.5in}
\setlength{\voffset}{-1in}
\setlength{\parskip}{.1in}

\newcommand{\meet}{\wedge}
\newcommand{\join}{\vee}

\renewcommand{\baselinestretch}{1.2}

\begin{document}

\title{Automatic Proofs and Counterexamples\\for Some Ortholattice Identities}

\author{{\it William McCune}\thanks
      {
      Supported by the Mathematical, Information,
      and Computational Sciences Division subprogram of the
      Office of Computational and Technology Research,
      U.S. Department of Energy, under Contract W-31-109-Eng-38.
      } \\
   Mathematics and Computer Science Division\\
   Argonne National Laboratory\\
   Argonne, Illinois, 60439, U.S.A.}

\maketitle


\sloppy

\begin{abstract}
\noindent
This note answers questions on
whether three identities known to hold
for orthomodular lattices are true also for ortholattices.
One identity is shown to fail by MACE, a program that searches for
counterexamples, an the other two are proved to hold by EQP,
an equational theorem prover.
The problems, from work in quantum logic,
were given to us by Norman Megill.
\end{abstract}

\noindent {\bf Keywords:} Automatic theorem proving, ortholattice,
quantum logic, theory of computation.

\section{Introduction}

An {\em ortholattice} is an algebra with a binary operation $\join$ (join)
and a unary operation $'$ (complement)
satisfying the following (independent) set of identities.
\begin{tabbing}
0000\=000000000000000000000000000\=\kill
\> $x \meet y = (x' \join y')'$  \> {(definition of meet)}\\
\> $x \join y = y \join x$\\
\> $(x \join y) \join z = x \join (y \join z)$\\
\> $x \join (x \meet y) = x$\\
\> $x'' = x$\\
\> $x \join (y \join y') = y \join y'$
\end{tabbing}
From these identities one can easily prove
commutativity and associativity of the meet operation,
idempotence of meet and join, and
the existence of a 1 and 0 with the usual Boolean properties.
Therefore I use the following identities as well
for ortholattices.
\begin{tabbing}
0000\=00000000000000000000000\=\kill
\> $x \meet y = y \meet x$\\
\> $(x \meet y) \meet z = x \meet (y \meet z)$\\
\> $x \join x = x$  \> $x \meet x = x$\\
\> $x \join x' = 1$ \> $x \meet x' = 0$\\
\> $x \join 1 = 1$  \> $x \meet 0 = 0$\\
\> $x \join 0 = x$  \> $x \meet 1 = x$
\end{tabbing}
An {\em orthomodular lattice} is an ortholattice satisfying
\begin{tabbing}
0000\=00000000000000000000000\=\kill
\> $x \join (x' \meet (x \join y)) = x \join y$.
\end{tabbing}

Consider the following three equations.
\begin{tabbing}
0000\=\kill

\> $((a \meet b') \join a')' \join ((a \meet b') \join ((a' \meet ((a \join b')
\meet (a \join b)))\ \join $\\ \` $ (a' \meet ((a \join b') \meet
(a \join b))'))) = 1$ \ \ \ (E1)\\[.2cm]

\> $(a \join ((a' \meet ((a \join b') \meet (a \join b))) \join (a' \meet
((a' \meet b) \join (a' \meet b'))))) = 1$ \` (E2)\\[.2cm]

\> $(((a' \meet b) \join (a' \meet b')) \join (a \meet (a' \join b)))'
\join (a' \join b) = 1$ \` (E3)

\end{tabbing}
These equations arose in work on quantum logic by
Mladen Pavi{\v{c}}i{\'{c}} and Norman Megill
\cite{megill-email,megill-submitted}.
Each equation was known to hold for
orthomodular lattices, but it was unknown whether any of
them holds for ortholattices.  Megill asked whether any of Argonne's
automated deduction programs could be used to solve the problems.

Equation E1 was shown to fail by the program MACE, which found
an ortholattice of order 10 violating E1.  Equations E2 and E3
were each shown to hold for ortholattices by the program EQP,
which produced equational proofs.
Equation E3 was proved for ortholattices by Megill (by hand),
independently and in parallel to our work,
shortly after he asked if our programs could prove it.

Quantum logic is meant to describe probability of events in
quantum dynamics (cf. Boolean algebra describes probability
in classical dynamics).  A.~R.~Marlow states \cite{marlow-oml}:
\begin{quotation}
\noindent Quantum theory is simply the replacement in standard probability
theory of event-as-subset-of-a-set (abelian, distributive) by
event-as-subspace-of-a-Hilbert-space (non-abelian, non-distributive).
\end{quotation}
However, working with quantum logic has been difficult; for example,
decidability of the word problem for orthomodular lattices is unknown.
R.~Goldblatt states\cite{goldblatt-oml}:
\begin{quotation}
\noindent ... further evidence of the intractability of quantum logic.
It is perhaps the first example of a natural and significant logic
that leaves the usual methods defeated.
\end{quotation}
The work of Pavi{\v{c}}i{\'{c}} and Megill is on using various
versions of the modus ponens rule with quantum logic.  Such
inference rules may affect computational efficiency of systems based on
quantum logic.

\subsection{The Programs EQP and MACE}

EQP \cite{eqp} is an automated theorem-proving program for
statements in first-order equational logic.  It has several
strategies for applying equational reasoning and searching
for proofs.  One of its strengths is that associativity and commutativity
of binary operations are built into the inference rules.  This feature
makes EQP perform well on many problems involving lattice-like structures.

MACE \cite{dp-quasi} is a program that searches for
finite models of first-order statements.  In practice,
it is limited to fairly simple statements without many
variables, and it usually cannot find large models.  Even with
these limitations, it is a valuable complement to our theorem provers.

(Our more well-known theorem prover Otter \cite{otter3,incarnations}
does not seem as effective as EQP for lattice-like problems because
Otter lacks associative-commutative unification and several valuable
paramodulation strategies.
See \cite{wm-rp:monograph} for several examples of using Otter
for this type of problem.)

\section{Equation E1}

I had no intuition about whether E1 could be proved for
ortholattices.  Hence, I put the programs to work in parallel, with
EQP searching for a proof and MACE searching for a counterexample.

To have MACE search for a counterexample, I gave it the
orthomodular axioms and asserted that there exist two elements, $a$ and $b$,
for which E1 fails.  Equation E1 is too complex for MACE,
but (because it is negated, with existentially quantified variables)
we can introduce names for subterms of E1, replacing it with
the following set of simpler equations.\footnote
{
The procedure of breaking up equations is straightforward;
it could easily be made automatic.
}
\begin{tabbing}
0000\=00000000000000000000000\=\kill
\> $a \meet b' = d_1$\\
\> $a \join b' = d_2$\\
\> $a \join b = d_3$\\
\> $a' = d_4$\\
\> $d_2 \meet d_3 = d_5$\\
\> $d_4 \meet d_5' = d_6$\\
\> $d_4 \meet d_5 = d_7$\\
\> $d_7 \join d_6 = d_8$\\
\> $(d_1 \join d_4)' \join (d_1 \join d_8) \neq 1$
\end{tabbing}
The ortholattice identities listed in the introduction 
involving 0, 1, and idempotence were included as well,
because such simple equations reduce the search space
that MACE must explore.

MACE was iterated, looking for models (i.e., ortholattices
violating E1) of orders 1, 2, $\ldots$.
The search spaces were quickly exhausted up through order 6 without
finding any models.\footnote
{
MACE is designed to be complete; that is, if no models are found for order $n$,
then there shouldn't be any.  Of course, proof by exhaustive search
is especially questionable.
}
Order 8 was exhausted, without models, in about 10 minutes using 15 megabytes
of memory.\footnote
{
All MACE and EQP searches were run on a 180 MHz i686 processor
with 128 megabytes of RAM, running the Linux operating system.
MACE and EQP are written in the C programming language.
}
A counterexample of order 10 was found in about 15 minutes using 84 megabytes.
Table~1 shows the model as produced by MACE, and Figure~\ref{fig:m10}
shows the corresponding ortholattice diagram.
% \newpage
{\small
\begin{table}[htbp] \centering \label{tab:m10}
\tabcolsep=4pt
\caption{Ortholattice violating E1}
\begin{tabular}{r|c}
$a$   & 2 \\
$b$   & 8 \\
$d_1$ & 7 \\
$d_2$ & 1 \\
$d_3$ & 5 \\
$d_4$ & 3 \\
$d_5$ & 5 \\
$d_6$ & 4 \\
$d_7$ & 0 \\
$d_8$ & 4
\end{tabular}
\hspace{.2cm}
\begin{tabular}{c|cccccccccc}
$\meet$ & 0 & 1 & 2 & 3 & 4 & 5 & 6 & 7 & 8 & 9\\
\hline
0 & 0 & 0 & 0 & 0 & 0 & 0 & 0 & 0 & 0 & 0\\
1 & 0 & 1 & 2 & 3 & 4 & 5 & 6 & 7 & 8 & 9\\
2 & 0 & 2 & 2 & 0 & 0 & 2 & 0 & 7 & 0 & 7\\
3 & 0 & 3 & 0 & 3 & 4 & 0 & 3 & 0 & 0 & 4\\
4 & 0 & 4 & 0 & 4 & 4 & 0 & 4 & 0 & 0 & 4\\
5 & 0 & 5 & 2 & 0 & 0 & 5 & 8 & 7 & 8 & 7\\
6 & 0 & 6 & 0 & 3 & 4 & 8 & 6 & 0 & 8 & 4\\
7 & 0 & 7 & 7 & 0 & 0 & 7 & 0 & 7 & 0 & 7\\
8 & 0 & 8 & 0 & 0 & 0 & 8 & 8 & 0 & 8 & 0\\
9 & 0 & 9 & 7 & 4 & 4 & 7 & 4 & 7 & 0 & 9
\end{tabular}
\hspace{.2cm}
\begin{tabular}{c|cccccccccc}
$\join$ & 0 & 1 & 2 & 3 & 4 & 5 & 6 & 7 & 8 & 9\\
\hline
0 & 0 & 1 & 2 & 3 & 4 & 5 & 6 & 7 & 8 & 9\\
1 & 1 & 1 & 1 & 1 & 1 & 1 & 1 & 1 & 1 & 1\\
2 & 2 & 1 & 2 & 1 & 1 & 5 & 1 & 2 & 5 & 1\\
3 & 3 & 1 & 1 & 3 & 3 & 1 & 6 & 1 & 6 & 1\\
4 & 4 & 1 & 1 & 3 & 4 & 1 & 6 & 9 & 6 & 9\\
5 & 5 & 1 & 5 & 1 & 1 & 5 & 1 & 5 & 5 & 1\\
6 & 6 & 1 & 1 & 6 & 6 & 1 & 6 & 1 & 6 & 1\\
7 & 7 & 1 & 2 & 1 & 9 & 5 & 1 & 7 & 5 & 9\\
8 & 8 & 1 & 5 & 6 & 6 & 5 & 6 & 5 & 8 & 1\\
9 & 9 & 1 & 1 & 1 & 9 & 1 & 1 & 9 & 1 & 9
\end{tabular}
\hspace{.2cm}
\begin{tabular}{c|c}
$'$ \\
\hline
0 & 1\\
1 & 0\\
2 & 3\\
3 & 2\\
4 & 5\\
5 & 4\\
6 & 7\\
7 & 6\\
8 & 9\\
9 & 8
\end{tabular}
\end{table}
}

\begin{figure}[htbp] \centering
% For the figure, you can use either the encapsulated PostScript
% file figure.eps, or the LaTeX picture file figure.tex.
% I recommend the eps file, because it is scaled to a better size.
\mbox{\epsfxsize=4cm\epsfbox{figure.eps}}
% \input{figure}
\caption{Ortholattice violating E1} \label{fig:m10}
\end{figure}

\section{Equation E2}

As with E1, I had no intuition about whether E2 holds for
ortholattices.  I started a proof search with EQP.
Before the counterexample search with MACE was even started,
EQP had found a proof.

As usual, I directed EQP to search for a proof by contradiction,
asserting the existence of elements $a$ and $b$ for which
E2 fails.  EQP found the proof below in about 4 seconds.

The justification ``$m \rightarrow n$'' indicates
associative-commutative paramodulation from $m$ into $n$, that is,
equality substitution, using (an instance of) $m$, into a subterm of
(an instance of) $n$; ``simp:i,j,$\ldots$'' indicates
associative-commutative simplification with $i, j, \ldots$; and
``flip'' indicates that the equation is reversed so that the more
complex side is on the left.

\begin{tabbing}
\=000000\=\kill
\> 1 \> $x'' = x$  \\
\> 3 \> $(x \meet y) \join x = x$  \\
\> 4 \> $(x' \join y')' = x \meet y$ \\
\> 7 \> $x' \join x = 1$  \\
\> 13 \> $a \join ((a' \meet ((b \meet a') \join (b' \meet a'))) \join (a' \meet ((b \join a) \meet (a \join b')))) \neq 1$  \\
\> 15 \> $(x' \join y)' = y' \meet x$ \` [1 $\rightarrow$ 4] \\
\> 19 \> $(x' \meet y)' = y' \join x$ \` [15 $\rightarrow$ 1] \\
\> 20 \> $x' \meet y' = (x \join y)'$ \` [1 $\rightarrow$ 15,flip] \\
\> 21 \> $a \join ((a' \meet ((b \join a)' \join (b \meet a'))) \join (a' \meet ((b \join a) \meet (a \join b')))) \neq 1$ \` [13,simp:20] \\
\> 24 \> $(x' \join y) \meet y = y$ \` [3 $\rightarrow$ 15,simp:1,19,flip] \\
\> 26 \> $(x \join y) \meet y = y$ \` [1 $\rightarrow$ 24] \\
\> 27 \> $x' \join ((y' \meet x) \join y) = 1$ \` [15 $\rightarrow$ 7] \\
\> 30 \> $((x' \meet y) \join z)' = z' \meet (y' \join x)$ \` [15 $\rightarrow$ 15] \\
\> 32 \> $((x \join y) \meet z) \join (y \meet z) = (x \join y) \meet z$ \` [26' $\rightarrow$ 3] \\
\> 120 \> $x' \meet (y' \join (z' \meet u)) = (((u' \join z) \meet y) \join x)'$ \` [19 $\rightarrow$ 30,flip] \\
\> 121 \> $a \join ((a \join ((b \join a) \meet (a \join b')))' \join (a' \meet ((b \join a) \meet (a \join b')))) \neq 1$ \` [21,simp:120] \\
\> 161 \> $((x \join y) \meet (y \join z)) \join y = (x \join y) \meet (y \join z)$ \` [26 $\rightarrow$ 32] \\
\> 162 \> $1 \neq 1$ \` [121,simp:161,27] \\
\end{tabbing}
The search strategy is summarized in the following points.
See \cite{eqp} further for details on these EQP features.
\begin{itemize}
\item The pair algorithm.
At each iteration of the search loop, a pair of equations
was selected for application of the inference rule.  
\item A selection ratio of four.
Through four iterations of the search loop, the shortest pair of
equations was selected, then the oldest pair of equations was
selected, and so on.  In other words, the strategy was four parts
shortest-first to one part breadth-first.
\item Basic paramodulation \cite{bachmair:basic}.
This restriction on application
of the inference rule prevented substitution of terms that
arise from instantiation alone.  Such inferences are redundant.
\item Prime paramodulation.  This restriction prevented
application of the inference rule if any term in the substitution
was reducible by the current set of equations.  Such inferences
are redundant.
\item The super-0 limit on associative-commutative (AC) unifiers.
When associativity and commutativity of a binary operation are
built into the inference process, a great (doubly exponential)
number of inferences can be made from a given pair of equations.
The super-0 method prevented inferences involving complicated
AC substitutions.
Our implementation of the method is incomplete, because
it simply discards the complicated AC substitutions; a complete
implementation that orders substitutions and backtracks could be made
to perform in a similar way the to current implementation.
\item Simplification.  An equation was used as a rewrite rule
if the left-hand side had more symbols than the right
and if no variable had more occurrences on the right-hand side.
\item Weight limit.  No limit was placed on the size of retained equations.
\end{itemize}

\section{Equation E3}

Again, since I had no intuition about whether E3 holds for
ortholattices, I started proof and counterexample searches in
parallel.  In about 15 minutes, MACE exhausted the ortholattices up
through order 8 without finding one that violates E3; then it
was set to work on order 10.  A proof search with EQP was started
using the same strategy that succeeded for E2.
Two days later EQP reported the following proof.
(The MACE and EQP jobs ran concurrently on the same processor;
the EQP process time was about 22.4 hours.)

% UNIT CONFLICT from 22528 and x=x at 80696.70 seconds.
\begin{tabbing}
\=000000\=\kill
\> 1 \> $x'' = x$  \\
\> 2 \> $x' \join (x \join y) = x' \join x$  \\
\> 3 \> $(x \meet y) \join x = x$  \\
\> 4 \> $(x' \join y')' = x \meet y$ \\
\> 7 \> $x' \join x = 1$  \\
\> 8 \> $1 \join x = 1$ \` [2,simp:7,7] \\
\> 13 \> $b \join (a' \join ((b \meet a') \join ((a \meet (b \join a')) \join (b' \meet a')))') \neq 1$  \\
\> 14 \> $x' \join y' = (x \meet y)'$ \` [4 $\rightarrow$ 1,flip] \\
\> 15 \> $b \join (a \meet ((b \meet a') \join ((a \meet (b \join a')) \join (b' \meet a'))))' \neq 1$ \` [13,simp:14] \\
\> 16 \> $(x' \join y)' = y' \meet x$ \` [1 $\rightarrow$ 4] \\
\> 22 \> $(x' \meet y)' = y' \join x$ \` [16 $\rightarrow$ 1] \\
\> 23 \> $x' \meet y' = (x \join y)'$ \` [1 $\rightarrow$ 16,flip] \\
\> 24 \> $b \join (a \meet ((b \join a)' \join ((b \meet a') \join (a \meet (b \join a')))))' \neq 1$ \` [15,simp:23] \\
\> 25 \> $(x' \join y) \meet y = y$ \` [3 $\rightarrow$ 16,simp:1,22,flip] \\
\> 27 \> $(x \join y) \meet y = y$ \` [1 $\rightarrow$ 25] \\
\> 28 \> $x' \join ((y' \meet x) \join y) = 1$ \` [16 $\rightarrow$ 7] \\
\> 31 \> $((x \join y) \meet z) \join (y \meet z) = (x \join y) \meet z$ \` [27' $\rightarrow$ 3] \\
\> 32 \> $((x \meet y) \join z) \meet (y \join z) = (x \meet y) \join z$ \` [3' $\rightarrow$ 27] \\
\> 33 \> $((x' \meet y) \join z)' = z' \meet (y' \join x)$ \` [16 $\rightarrow$ 16] \\
\> 38 \> $((x' \join y) \meet z)' \join x = z' \join x$ \` [27' $\rightarrow$ 22,simp:22,flip] \\
\> 146 \> $(x \meet y)' \meet (y' \join (x' \meet z)) = y' \join (x' \meet z)$ \` [14 $\rightarrow$ 32] \\
\> 174 \> $x' \meet (y' \join (z' \meet u)) = (((u' \join z) \meet y) \join x)'$ \` [22 $\rightarrow$ 33,flip] \\
\> 175 \> $((x' \join y) \meet z)' = z' \join (y' \meet x)$ \` [146,simp:174,31] \\
\> 281 \> $x' \join ((y' \meet ((z' \join u) \meet x)) \join (y \join z)) = 1$ \` [38' $\rightarrow$ 28',simp:8] \\
\> 2662 \> $x' \join (((y \meet z)' \meet ((z' \join u) \meet x)) \join z) = 1$ \` [3' $\rightarrow$ 281] \\
\> 2663 \> $(((x \meet y) \join z)' \meet (y' \join u)) \join (y \join z) = 1$ \` [1 $\rightarrow$ 2662,simp:23] \\
\> 2664 \> $x' \join ((((x' \meet y) \join z)' \meet (x \join u)) \join z) = 1$ \` [1 $\rightarrow$ 2663] \\
\> 3141 \> $x' \join ((((x' \meet y) \join ((x' \join z) \meet u))' \meet (x \join v)) \join z) = 1$ \` [2664' $\rightarrow$ 3',simp:8,flip] \\
\> 22528 \> $1 \neq 1$ \` [175 $\rightarrow$ 24,simp:3141] \\
\end{tabbing}

\section{Conclusion}

These results are not deep, but they illustrate one kind of automatic
deduction assistance that is becoming available to mathematicians and
logicians.

The programs EQP and MACE, and the input files that produce these results are
available on the Web at the following location.
\begin{verbatim}
    http://www.mcs.anl.gov/home/mccune/ar/ortholattice/
\end{verbatim}

\section*{Appendix}

I sent the results of the programs to Megill, who replied:

\begin{quotation} \noindent
For your interest, [your lattice] is actually used to show that the
following equation does not have an ortholattice proof.  The equation
I sent you [E1] was the ``missing piece'' of a proof that I was attempting to
construct.
\hspace{.1cm} \ldots \hspace{.2cm}
Specifically, this is the lattice algebra mapping of axiom A14 of a system
of quantum logic of Kalmbach, {\em Orthomodular Lattices}, p. 240.
{\small
\[
\begin{array}{ll}
( ( ( a' \meet b )' \join ( ( ( a' \join ( ( ( a' \join b
) \meet ( a' \join b' ) ) \meet ( a \join ( a' \meet b ) ) ) ) \meet ( a' \\
\join ( ( ( a' \join b ) \meet ( a' \join b' ) ) \meet ( a \join ( a' \meet
b ) ) )' ) ) \meet ( a \join ( a' \meet ( ( ( a' \join b ) \meet ( a' \join \\
b' ) ) \meet ( a \join ( a' \meet b ) ) ) ) ) ) ) \meet ( ( a' \meet b
)' \join ( ( ( a' \join ( ( ( a' \join b ) \meet ( a' \join b' ) ) \meet \\
( a \join ( a' \meet b ) ) ) ) \meet ( a' \join ( ( ( a' \join b ) \meet
( a' \join b' ) ) \meet ( a \join ( a' \meet b ) ) )' ) ) \meet ( a \join  & \mbox{(E4)}\\
( a' \meet ( ( ( a' \join b ) \meet ( a' \join b' ) ) \meet ( a \join ( a'
\meet b ) ) ) ) ) )' ) ) \meet ( ( a' \meet b ) \join ( ( a' \meet b )' \\
\meet ( ( ( a' \join ( ( ( a' \join b ) \meet ( a' \join b' ) ) \meet ( a
\join ( a' \meet b ) ) ) ) \meet ( a' \join ( ( ( a' \join b ) \meet ( a' \\
\join b' ) ) \meet ( a \join ( a' \meet b ) ) )' ) ) \meet ( a \join ( a'
\meet ( ( ( a' \join b ) \meet ( a' \join b' ) ) \meet ( a \join ( a' \meet b \\
) ) ) ) ) ) ) ) = 1.
\end{array}
\]
}
\end{quotation}
Of course, I wondered (1) whether the same ortholattice
violating E1 also violates this equation, (2) if so, whether
MACE could find it directly, and (3) if not, whether
MACE could find another one.

As with E1, the denial of E4 was broken up by naming subterms
so that MACE could cope with it.
No counterexamples were found among the ortholattices up through
order 8.  The order 10 search produced an ortholattice violating E4,
isomorphic to the one violating E1 (Table 1 and Figure 1).\footnote
{
The first MACE search with E4 required more memory ($>100$ megabytes) than
the successful E1 MACE search had used (84 megabytes), and I had to find
a way reduce the space requirement.  Fortunately, two of the
larger equations (associativity of meet and 
$x \join (y \join y') = y \join y'$) could be omitted, because they
depend on the other axioms and lemmas;  this allowed the search
to run in less than 70 megabytes.
}

As a double check, a MACE run was set up to verify that the
ortholattice (as written in Table~1) violates E4 by including
constraints corresponding to the table.  This type of MACE run simply
verifies that an interpretation is satisfies a statement.
The verification succeeded.

\bibliographystyle{plain}

% \bibliography{/home/mccune/papers/bib/master}

\begin{thebibliography}{10}

\bibitem{bachmair:basic}
L.~Bachmair, H.~Ganzinger, C.~Lynch, and W.~Snyder.
\newblock Basic paramodulation and superposition.
\newblock In D.~Kapur, editor, {\em Proceedings of the 11th International
  Conference on Automated Deduction, Lecture Notes in Artificial Intelligence,
  Vol. 607}, pages 462--476. Springer-Verlag, 1992.

\bibitem{goldblatt-oml}
R.~Goldblatt.
\newblock Orthomodularity is not elementary.
\newblock {\em J. Symbolic Logic}, 49(2):401--404, 1984.

\bibitem{marlow-oml}
A.~R. Marlow.
\newblock Orthomodular structures and physical theory.
\newblock In {\em Mathematical Foundations of Quantum Theory}, pages 59--70.
  Academic Press, 1977.

\bibitem{dp-quasi}
W.~McCune.
\newblock A {D}avis-{P}utnam program and its application to finite first-order
  model search: Quasigroup existence problems.
\newblock Tech. Report ANL/MCS-TM-194, Argonne National Laboratory, Argonne,
  IL, May 1994.

\bibitem{otter3}
W.~McCune.
\newblock Otter 3.0 {R}eference {M}anual and {G}uide.
\newblock Tech. Report ANL-94/6, Argonne National Laboratory, Argonne, IL,
  1994.

\bibitem{eqp}
W.~McCune.
\newblock 33 basic test problems: A practical evaluation of some paramodulation
  strategies.
\newblock In Robert Veroff, editor, {\em Automated Reasoning and its
  Applications: Essays in Honor of Larry Wos}, chapter~5, pages 71--114. MIT
  Press, 1997.

\bibitem{wm-rp:monograph}
W.~McCune and R.~Padmanabhan.
\newblock {\em Automated Deduction in Equational Logic and Cubic Curves},
  volume 1095 of {\em Lecture Notes in Computer Science (AI subseries)}.
\newblock Springer-Verlag, Berlin, 1996.

\bibitem{incarnations}
W.~McCune and L.~Wos.
\newblock Otter: {T}he {CADE}-13 {C}ompetition incarnations.
\newblock {\em J. Automated Reasoning}, 18(2):211--220, 1997.

\bibitem{megill-email}
N.~Megill, Sept. 1997.
\newblock Correspondence by electronic mail.

\bibitem{megill-submitted}
Mladen Pavi{\v{c}}i{\'{c}} and Norman Megill.
\newblock Binary orthologic with modus ponens is either orthomodular or
  distributive.
\newblock Submitted, November 1997.

\end{thebibliography}


\end{document}
