doc-src/Sledgehammer/sledgehammer.tex
 changeset 43007 b48aa3492f0b parent 43005 c96f06bffd90 child 43008 bb212c2ad238
equal inserted replaced
43006:ff631c45797e 43007:b48aa3492f0b
   248 \prew
   248 \prew
   249 \slshape
   249 \slshape
   250 Sledgehammer: \textit{e}'' for subgoal 1: \\
   250 Sledgehammer: \textit{e}'' for subgoal 1: \\
   251 $[a] = [b] \,\Longrightarrow\, a = b$ \\
   251 $[a] = [b] \,\Longrightarrow\, a = b$ \\
   252 Try this command: \textbf{by} (\textit{metis last\_ConsL}). \\
   252 Try this command: \textbf{by} (\textit{metis last\_ConsL}). \\
   253 To minimize the number of lemmas, try this: \\
   253 To minimize: \textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{e}] (\textit{last\_ConsL}). \\[3\smallskipamount]
   254 \textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{e}] (\textit{last\_ConsL}). \\[3\smallskipamount]

   255 %
   254 %
   256 Sledgehammer: \textit{vampire}'' for subgoal 1: \\
   255 Sledgehammer: \textit{vampire}'' for subgoal 1: \\
   257 $[a] = [b] \,\Longrightarrow\, a = b$ \\
   256 $[a] = [b] \,\Longrightarrow\, a = b$ \\
   258 Try this command: \textbf{by} (\textit{metis hd.simps}). \\
   257 Try this command: \textbf{by} (\textit{metis hd.simps}). \\
   259 To minimize the number of lemmas, try this: \\
   258 To minimize: \textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{vampire}] (\textit{hd.simps}). \\[3\smallskipamount]
   260 \textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{vampire}] (\textit{hd.simps}). \\[3\smallskipamount]

   261 %
   259 %
   262 Sledgehammer: \textit{spass}'' for subgoal 1: \\
   260 Sledgehammer: \textit{spass}'' for subgoal 1: \\
   263 $[a] = [b] \,\Longrightarrow\, a = b$ \\
   261 $[a] = [b] \,\Longrightarrow\, a = b$ \\
   264 Try this command: \textbf{by} (\textit{metis list.inject}). \\
   262 Try this command: \textbf{by} (\textit{metis list.inject}). \\
   265 To minimize the number of lemmas, try this: \\
   263 To minimize: \textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{spass}]~(\textit{list.inject}). \\[3\smallskipamount]
   266 \textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{spass}]~(\textit{list.inject}). \\[3\smallskipamount]

   267 %
   264 %
   268 %Sledgehammer: \textit{remote\_waldmeister}'' for subgoal 1: \\
   265 %Sledgehammer: \textit{remote\_waldmeister}'' for subgoal 1: \\
   269 %$[a] = [b] \,\Longrightarrow\, a = b$ \\
   266 %$[a] = [b] \,\Longrightarrow\, a = b$ \\
   270 %Try this command: \textbf{by} (\textit{metis hd.simps insert\_Nil}). \\
   267 %Try this command: \textbf{by} (\textit{metis hd.simps insert\_Nil}). \\
   271 %To minimize the number of lemmas, try this: \\
   268 %To minimize: \textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{remote\_waldmeister}] \\
   272 %\textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{remote\_waldmeister}] \\

   273 %\phantom{\textbf{sledgehammer}~}(\textit{hd.simps insert\_Nil}). \\[3\smallskipamount]
   269 %\phantom{\textbf{sledgehammer}~}(\textit{hd.simps insert\_Nil}). \\[3\smallskipamount]
   274 %
   270 %
   275 Sledgehammer: \textit{remote\_sine\_e}'' for subgoal 1: \\
   271 Sledgehammer: \textit{remote\_sine\_e}'' for subgoal 1: \\
   276 $[a] = [b] \,\Longrightarrow\, a = b$ \\
   272 $[a] = [b] \,\Longrightarrow\, a = b$ \\
   277 Try this command: \textbf{by} (\textit{metis hd.simps}). \\
   273 Try this command: \textbf{by} (\textit{metis hd.simps}). \\
   278 To minimize the number of lemmas, try this: \\
   274 To minimize: \textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{remote\_sine\_e}] \\
   279 \textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{remote\_sine\_e}]~(\textit{hd.simps}). \\[3\smallskipamount]
   275 \phantom{To minimize: }(\textit{hd.simps}). \\[3\smallskipamount]
   280 %
   276 %
   281 Sledgehammer: \textit{remote\_z3}'' for subgoal 1: \\
   277 Sledgehammer: \textit{remote\_z3}'' for subgoal 1: \\
   282 $[a] = [b] \,\Longrightarrow\, a = b$ \\
   278 $[a] = [b] \,\Longrightarrow\, a = b$ \\
   283 Try this command: \textbf{by} (\textit{metis hd.simps}). \\
   279 Try this command: \textbf{by} (\textit{metis hd.simps}). \\
   284 To minimize the number of lemmas, try this: \\
   280 To minimize: \textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{remote\_z3}]~(\textit{hd.simps}).
   285 \textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{remote\_z3}]~(\textit{hd.simps}).

   286 \postw
   281 \postw
   287
   282
   288 Sledgehammer ran E, SInE-E, SPASS, Vampire, %Waldmeister,
   283 Sledgehammer ran E, SInE-E, SPASS, Vampire, %Waldmeister,
   289 and Z3 in parallel.
   284 and Z3 in parallel.
   290 Depending on which provers are installed and how many processor cores are
   285 Depending on which provers are installed and how many processor cores are
   354 if you are the kind of user who can think clearly while ATPs are active.
   349 if you are the kind of user who can think clearly while ATPs are active.
   355
   350
   356 \item[$\bullet$] \textbf{\textit{full\_types}} (\S\ref{problem-encoding})
   351 \item[$\bullet$] \textbf{\textit{full\_types}} (\S\ref{problem-encoding})
   357 specifies whether type-sound encodings should be used. By default, Sledgehammer
   352 specifies whether type-sound encodings should be used. By default, Sledgehammer
   358 employs a mixture of type-sound and type-unsound encodings, occasionally
   353 employs a mixture of type-sound and type-unsound encodings, occasionally
   359 yielding unsound ATP proofs. (SMT solver proofs should always be sound, although
   354 yielding unsound ATP proofs. In contrast, SMT solver proofs should always be
   360 we occasionally find soundness bugs in the solvers.)
   355 sound.
   361
   356
   362 \item[$\bullet$] \textbf{\textit{max\_relevant}} (\S\ref{relevance-filter})
   357 \item[$\bullet$] \textbf{\textit{max\_relevant}} (\S\ref{relevance-filter})
   363 specifies the maximum number of facts that should be passed to the provers. By
   358 specifies the maximum number of facts that should be passed to the provers. By
   364 default, the value is prover-dependent but varies between about 150 and 1000. If
   359 default, the value is prover-dependent but varies between about 150 and 1000. If
   365 the provers time out, you can try lowering this value to, say, 100 or 50 and see
   360 the provers time out, you can try lowering this value to, say, 100 or 50 and see
   527 \textit{metis} if the proof obviously requires type information.
   522 \textit{metis} if the proof obviously requires type information.
   528
   523
   529 If you see the warning
   524 If you see the warning
   530
   525
   531 \prew
   526 \prew
   532 \textsl
   527 \slshape
   533 Metis: Falling back on \textit{metisFT}''.
   528 Metis: Falling back on \textit{metisFT\/}''.
   534 \postw
   529 \postw
   535
   530
   536 in a successful Metis proof, you can advantageously replace the \textit{metis}
   531 in a successful Metis proof, you can advantageously replace the \textit{metis}
   537 call with \textit{metisFT}.
   532 call with \textit{metisFT}.
   538
   533