doc-src/Ref/classical.tex
 changeset 8284 95c022a866ca parent 8136 8c65f3ca13f2 child 8702 78b7010db847
equal inserted replaced
8283:0a319c5746eb 8284:95c022a866ca
   468 The two tactics differ on how they bound the number of unsafe steps used in a
   468 The two tactics differ on how they bound the number of unsafe steps used in a
   469 proof.  While \texttt{blast_tac} starts with a bound of zero and increases it
   469 proof.  While \texttt{blast_tac} starts with a bound of zero and increases it
   470 successively to~20, \texttt{Blast.depth_tac} applies a user-supplied search bound.
   470 successively to~20, \texttt{Blast.depth_tac} applies a user-supplied search bound.
   471 \begin{ttdescription}
   471 \begin{ttdescription}
   472 \item[\ttindexbold{blast_tac} $cs$ $i$] tries to prove
   472 \item[\ttindexbold{blast_tac} $cs$ $i$] tries to prove
   473   subgoal~$i$ using iterative deepening to increase the search bound.
   473   subgoal~$i$, increasing the search bound using iterative

   474   deepening~\cite{korf85}.
   474
   475
   475 \item[\ttindexbold{Blast.depth_tac} $cs$ $lim$ $i$] tries
   476 \item[\ttindexbold{Blast.depth_tac} $cs$ $lim$ $i$] tries
   476   to prove subgoal~$i$ using a search bound of $lim$.  Often a slow
   477   to prove subgoal~$i$ using a search bound of $lim$.  Sometimes a slow
   477   proof using \texttt{blast_tac} can be made much faster by supplying the
   478   proof using \texttt{blast_tac} can be made much faster by supplying the
   478   successful search bound to this tactic instead.
   479   successful search bound to this tactic instead.
   479
   480
   480 \item[set \ttindexbold{Blast.trace};] \index{tracing!of classical prover}
   481 \item[set \ttindexbold{Blast.trace};] \index{tracing!of classical prover}
   481   causes the tableau prover to print a trace of its search.  At each step it
   482   causes the tableau prover to print a trace of its search.  At each step it