\doc{Operational syntax and semantics}
\ref{system}

The basis for each proof in LP is a logical system that contains a collection
of facts (axioms, hypotheses, and previously proved theorems) available for use
in that proof.  There is a separate logical system, known as a proof context,
for the proof of each conjecture and subgoal.
\p
The facts in a logical system have both semantic content (expressed by formulas
in first-order logic) and operational content.  For more information about this
operational content, see:
\begin{itemize}
\item \dlink{formula}{Formulas}
\item \dlink{inconsistency}{Inconsistencies}
\item \dlink{rewrite-rule}{Rewrite rules}
\item \dlink{operator-theory}{Operator theories}
\item \dlink{induction-rule}{Induction rules}
\item \dlink{deduction-rule}{Deduction rules}
\end{itemize}