\doc{Release 3.1b}
\ref{release3_1b}

The following bugs in Version 3.1a have been fixed in Version 3.1b.
\begin{description}
\dt 95-014
\dd
LP failed to normalize some rewrite rules in response to the \fq{normalize}
command.  In particular, it failed to normalize a rewrite rule when the left
side of that rewrite rule could be reduced, but no further reductions were
possible.
\dt 95-015
\dd
LP incorrectly (and unsoundly) eliminated some subterms when reducing formulas
such as \fq{a = (r = (b = b'))} that contain multiple occurrences of equality
between boolean subformulas.
\dt 95-016
\dd
The experimental version of LP (invoked by the command \fq{lp -e}) failed if a
\fq{register} command was issued while a proof was in progress.

\end{description}

In addition, the following improvements have been made in Version 3.1b.

\begin{itemize}
\item

\end{itemize}