\doc{Logical syntax and semantics}
\ref{logical}

LP is a proof assistant for multisorted first-order logic.  Except for the fact
that it provides a rich set of notations for functions, LP is based on the 
syntax and semantics for first-order logic found in many textbooks.  For a
description of this syntax and semantics, see:

\begin{itemize}
\item \dlink{../symbols/syntax}{Conventions} for describing LP's syntax
\item \dlink{../symbols/symbols}{Symbols}
\item \dlink{sort}{Sorts}
\item \dlink{variable}{Variables}
\item \dlink{operator}{Operators}
\item \dlink{quantifier}{Quantifiers}
\item \dlink{term}{Terms}
\item \dlink{formula}{Formulas}
\end{itemize}