diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/Micromega.tex | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/doc/refman/Micromega.tex b/doc/refman/Micromega.tex index 00e7c04138..a43cd15b06 100644 --- a/doc/refman/Micromega.tex +++ b/doc/refman/Micromega.tex @@ -8,7 +8,8 @@ Section~\ref{sec:psatz-back} presents some background explaining the proof princ % Section~\ref{sec:lia} explains how to get a complete procedure for linear integer arithmetic. -\section{The {\tt psatz} tactic in a hurry} +\asection{The {\tt psatz} tactic in a hurry} +\tacindex{psatz} \label{sec:psatz-hurry} Load the {\tt Psatz} module ({\tt Require Psatz}.). This module defines the tactics: {\tt lia}, {\tt psatzl D}, %{\tt sos D} @@ -54,7 +55,7 @@ The following table details for each domain $D \in \{\mathbb{Z},\mathbb{Q},\math \end{array} \] -\section{\emph{Positivstellensatz} refutations} +\asection{\emph{Positivstellensatz} refutations} \label{sec:psatz-back} The name {\tt psatz} is an abbreviation for \emph{positivstellensatz} -- literally positivity theorem -- which @@ -121,7 +122,8 @@ refutation. %% This amounts to searching for $p$ in the cone without generators \emph{i.e.}, $Cone(\{\})$. % -\section{ {\tt lia} : the linear integer arithmetic tactic } +\asection{ {\tt lia} : the linear integer arithmetic tactic } +\tacindex{lia} \label{sec:lia} The tactic {\tt lia} offers an alternative to the {\tt omega} and {\tt romega} tactic (see |