\doc{Introduction}
\ref{LP}
\ref{overview}
\ref{introduction}

LP is an interactive theorem proving system for multisorted first-order logic.
It is currently used at MIT and elsewhere to reason about designs for circuits,
concurrent algorithms, hardware, and software.  Unlike most theorem provers,
which attempt to find proofs automatically for correctly stated conjectures, LP
is intended to assist users in finding and correcting flaws in
conjectures---the predominant activity in the early stages of the design
process.
\p
LP works efficiently on large problems, has many important user amenities, and
can be used by relatively naive users.  It was developed and is being
maintained by Stephen J. Garland and John V. Guttag at the MIT Laboratory for
Computer Science.
\p
For a general introduction to LP, see the following topics.
\p
\begin{itemize}
\item \dlink{news/distribution}{Getting} the current distribution of LP
\item \dlink{news/news}{News} about recent changes to LP
\item Using LP
\begin{itemize}
\item \dlink{misc/sample}{Some sample proofs}
\item \dlink{logic/logic}{Logical syntax and semantics}
\item \dlink{logic/system}{Operational syntax and semantics}
\item \dlink{proof/forward}{Forward inference mechanisms} for using axioms
\item \dlink{proof/backward}{Backward inference mechanisms} for proving conjectures
\item \dlink{commands/commands}{Commands} recognized by LP
\end{itemize}
\item \dlink{misc/philosophy}{Design philosophy}
\item \dlink{contents}{Table of contents for this documentation}
\end{itemize}
This is a preliminary version of the documentation for LP.  A more polished
version, both in hypertext and in hardcopy, will be available in early 1995.