# HG changeset patch
# User blanchet
# Date 1306767638 -7200
# Node ID f1864c0bd165a7c4d7a6d20e8430d3f0261d7d5a
# Parent  da6f459a70215fe8d0248a33170337f6828e1c37
update minimization documentation

diff -r da6f459a7021 -r f1864c0bd165 doc-src/Sledgehammer/sledgehammer.tex
--- a/doc-src/Sledgehammer/sledgehammer.tex	Mon May 30 17:00:38 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Mon May 30 17:00:38 2011 +0200
@@ -249,34 +249,27 @@
 \slshape
 Sledgehammer: ``\textit{e}'' on goal \\
 $[a] = [b] \,\Longrightarrow\, a = b$ \\
-Try this: \textbf{by} (\textit{metis last\_ConsL}) (46 ms). \\
-To minimize: \textbf{sledgehammer} \textit{min} [\textit{e}] (\textit{last\_ConsL}). \\[3\smallskipamount]
+Try this: \textbf{by} (\textit{metis last\_ConsL}) (64 ms). \\[3\smallskipamount]
 %
 Sledgehammer: ``\textit{vampire}'' on goal \\
 $[a] = [b] \,\Longrightarrow\, a = b$ \\
-Try this: \textbf{by} (\textit{metis hd.simps}) (17 ms). \\
-To minimize: \textbf{sledgehammer} \textit{min} [\textit{vampire}] (\textit{hd.simps}). \\[3\smallskipamount]
+Try this: \textbf{by} (\textit{metis hd.simps}) (14 ms). \\[3\smallskipamount]
 %
 Sledgehammer: ``\textit{spass}'' on goal \\
 $[a] = [b] \,\Longrightarrow\, a = b$ \\
-Try this: \textbf{by} (\textit{metis list.inject}) (20 ms). \\
-To minimize: \textbf{sledgehammer} \textit{min} [\textit{spass}]~(\textit{list.inject}). \\[3\smallskipamount]
+Try this: \textbf{by} (\textit{metis list.inject}) (17 ms). \\[3\smallskipamount]
 %
 Sledgehammer: ``\textit{remote\_waldmeister}'' on goal \\
 $[a] = [b] \,\Longrightarrow\, a = b$ \\
-Try this: \textbf{by} (\textit{metis hd.simps insert\_Nil}) (25 ms). \\
-To minimize: \textbf{sledgehammer} \textit{min} [\textit{remote\_waldmeister}] \\
-\phantom{To minimize: \textbf{sledgehammer}~}(\textit{hd.simps insert\_Nil}). \\[3\smallskipamount]
+Try this: \textbf{by} (\textit{metis hd.simps}) (15 ms). \\[3\smallskipamount]
 %
 Sledgehammer: ``\textit{remote\_sine\_e}'' on goal \\
 $[a] = [b] \,\Longrightarrow\, a = b$ \\
-Try this: \textbf{by} (\textit{metis hd.simps}) (17 ms). \\
-To minimize: \textbf{sledgehammer} \textit{min} [\textit{remote\_sine\_e}]~(\textit{hd.simps}). \\[3\smallskipamount]
+Try this: \textbf{by} (\textit{metis hd.simps}) (18 ms). \\[3\smallskipamount]
 %
 Sledgehammer: ``\textit{remote\_z3}'' on goal \\
 $[a] = [b] \,\Longrightarrow\, a = b$ \\
-Try this: \textbf{by} (\textit{metis hd.simps}) (17 ms). \\
-To minimize: \textbf{sledgehammer} \textit{min} [\textit{remote\_z3}]~(\textit{hd.simps}).
+Try this: \textbf{by} (\textit{metis list.inject}) (20 ms).
 \postw
 
 Sledgehammer ran E, SInE-E, SPASS, Vampire, Waldmeister, and Z3 in parallel.
@@ -286,13 +279,11 @@
 where the goal's conclusion is a (universally quantified) equation.
 
 For each successful prover, Sledgehammer gives a one-liner proof that uses Metis
-or the \textit{smt} proof method. For Metis, timings are shown in parentheses,
-indicating how fast the call is. You can click the proof to insert it into the
-theory text. You can click the ``\textbf{sledgehammer} \textit{minimize}''
-command if you want to look for a shorter (and probably faster) proof. But here
-the proof found by Vampire is both short and fast already.
+or the \textit{smt} proof method. For Metis, approximate timings are shown in
+parentheses, indicating how fast the call is. You can click the proof to insert
+it into the theory text.
 
-You can ask Sledgehammer for an Isar text proof by passing the
+In addition, you can ask Sledgehammer for an Isar text proof by passing the
 \textit{isar\_proof} option (\S\ref{output-format}):
 
 \prew
@@ -526,21 +517,27 @@
 in a successful Metis proof, you can advantageously replace the \textit{metis}
 call with \textit{metisFT}.
 
-\point{Should I minimize the number of lemmas?}
+\point{Are generated proofs minimal?}
 
-In general, minimization is a good idea, because proofs involving fewer lemmas
-tend to be shorter as well, and hence easier to re-find by Metis. But the
-opposite is sometimes the case. Keep an eye on the timing information displayed
-next to the suggested Metis calls.
+Automatic provers frequently use many more facts than are necessary.
+Sledgehammer inclues a minimization tool that takes a set of facts returned by a
+given prover and repeatedly calls the same prover or Metis with subsets of those
+axioms in order to find a minimal set. Reducing the number of axioms typically
+improves Metis's speed and success rate, while also removing superfluous clutter
+from the proof scripts.
 
-\point{Why does the minimizer sometimes starts on its own?}
+In earlier versions of Sledgehammer, generated proofs were accompanied by a
+suggestion to invoke the minimization tool. This step is now performed
+implicitly if it can be done in a reasonable amount of time (something that can
+be guessed from the number of facts in the original proof and the time it took
+to find it or replay it).
 
-There are two scenarios in which this can happen. First, some provers (notably
-CVC3, Satallax, and Yices) do not provide proofs or sometimes provide incomplete
-proofs. The minimizer is then invoked to find out which facts are actually
-needed from the (large) set of facts that was initinally given to the prover.
-Second, if a prover returns a proof with lots of facts, the minimizer is invoked
-automatically since Metis would be unlikely to re-find the proof.
+In addition, some provers (notably CVC3, Satallax, and Yices) do not provide
+proofs or sometimes provide incomplete proofs. The minimizer is then invoked to
+find out which facts are actually needed from the (large) set of facts that was
+initinally given to the prover. Finally, if a prover returns a proof with lots
+of facts, the minimizer is invoked automatically since Metis would be unlikely
+to re-find the proof.
 
 \point{A strange error occurred---what should I do?}