307 For each successful prover, Sledgehammer gives a one-liner \textit{metis} or |
307 For each successful prover, Sledgehammer gives a one-liner \textit{metis} or |
308 \textit{smt} method call. Rough timings are shown in parentheses, indicating how |
308 \textit{smt} method call. Rough timings are shown in parentheses, indicating how |
309 fast the call is. You can click the proof to insert it into the theory text. |
309 fast the call is. You can click the proof to insert it into the theory text. |
310 |
310 |
311 In addition, you can ask Sledgehammer for an Isar text proof by passing the |
311 In addition, you can ask Sledgehammer for an Isar text proof by passing the |
312 \textit{isar\_proof} option (\S\ref{output-format}): |
312 \textit{isar\_proofs} option (\S\ref{output-format}): |
313 |
313 |
314 \prew |
314 \prew |
315 \textbf{sledgehammer} [\textit{isar\_proof}] |
315 \textbf{sledgehammer} [\textit{isar\_proofs}] |
316 \postw |
316 \postw |
317 |
317 |
318 When Isar proof construction is successful, it can yield proofs that are more |
318 When Isar proof construction is successful, it can yield proofs that are more |
319 readable and also faster than the \textit{metis} or \textit{smt} one-liners. |
319 readable and also faster than the \textit{metis} or \textit{smt} one-liners. |
320 This feature is experimental and is only available for ATPs. |
320 This feature is experimental and is only available for ATPs. |
364 specifies the maximum number of facts that should be passed to the provers. By |
364 specifies the maximum number of facts that should be passed to the provers. By |
365 default, the value is prover-dependent but varies between about 50 and 1000. If |
365 default, the value is prover-dependent but varies between about 50 and 1000. If |
366 the provers time out, you can try lowering this value to, say, 25 or 50 and see |
366 the provers time out, you can try lowering this value to, say, 25 or 50 and see |
367 if that helps. |
367 if that helps. |
368 |
368 |
369 \item[\labelitemi] \textbf{\textit{isar\_proof}} (\S\ref{output-format}) specifies |
369 \item[\labelitemi] \textbf{\textit{isar\_proofs}} (\S\ref{output-format}) specifies |
370 that Isar proofs should be generated, instead of one-liner \textit{metis} or |
370 that Isar proofs should be generated, instead of one-liner \textit{metis} or |
371 \textit{smt} proofs. The length of the Isar proofs can be controlled by setting |
371 \textit{smt} proofs. The length of the Isar proofs can be controlled by setting |
372 \textit{isar\_shrink\_factor} (\S\ref{output-format}). |
372 \textit{isar\_shrinkage} (\S\ref{output-format}). |
373 |
373 |
374 \item[\labelitemi] \textbf{\textit{timeout}} (\S\ref{timeouts}) controls the |
374 \item[\labelitemi] \textbf{\textit{timeout}} (\S\ref{timeouts}) controls the |
375 provers' time limit. It is set to 30 seconds, but since Sledgehammer runs |
375 provers' time limit. It is set to 30 seconds, but since Sledgehammer runs |
376 asynchronously you should not hesitate to raise this limit to 60 or 120 seconds |
376 asynchronously you should not hesitate to raise this limit to 60 or 120 seconds |
377 if you are the kind of user who can think clearly while ATPs are active. |
377 if you are the kind of user who can think clearly while ATPs are active. |
468 proof is too difficult for it. Metis's search is complete, so it should |
468 proof is too difficult for it. Metis's search is complete, so it should |
469 eventually find it, but that's little consolation. There are several possible |
469 eventually find it, but that's little consolation. There are several possible |
470 solutions: |
470 solutions: |
471 |
471 |
472 \begin{enum} |
472 \begin{enum} |
473 \item[\labelitemi] Try the \textit{isar\_proof} option (\S\ref{output-format}) to |
473 \item[\labelitemi] Try the \textit{isar\_proofs} option (\S\ref{output-format}) to |
474 obtain a step-by-step Isar proof where each step is justified by \textit{metis}. |
474 obtain a step-by-step Isar proof where each step is justified by \textit{metis}. |
475 Since the steps are fairly small, \textit{metis} is more likely to be able to |
475 Since the steps are fairly small, \textit{metis} is more likely to be able to |
476 replay them. |
476 replay them. |
477 |
477 |
478 \item[\labelitemi] Try the \textit{smt} proof method instead of \textit{metis}. |
478 \item[\labelitemi] Try the \textit{smt} proof method instead of \textit{metis}. |
502 strongly encouraged to report this to the author at \authoremail. |
502 strongly encouraged to report this to the author at \authoremail. |
503 |
503 |
504 \point{Why are the generated Isar proofs so ugly/broken?} |
504 \point{Why are the generated Isar proofs so ugly/broken?} |
505 |
505 |
506 The current implementation of the Isar proof feature, |
506 The current implementation of the Isar proof feature, |
507 enabled by the \textit{isar\_proof} option (\S\ref{output-format}), |
507 enabled by the \textit{isar\_proofs} option (\S\ref{output-format}), |
508 is highly experimental. Work on a new implementation has begun. There is a large body of |
508 is highly experimental. Work on a new implementation has begun. There is a large body of |
509 research into transforming resolution proofs into natural deduction proofs (such |
509 research into transforming resolution proofs into natural deduction proofs (such |
510 as Isar proofs), which we hope to leverage. In the meantime, a workaround is to |
510 as Isar proofs), which we hope to leverage. In the meantime, a workaround is to |
511 set the \textit{isar\_shrink\_factor} option (\S\ref{output-format}) to a larger |
511 set the \textit{isar\_shrinkage} option (\S\ref{output-format}) to a larger |
512 value or to try several provers and keep the nicest-looking proof. |
512 value or to try several provers and keep the nicest-looking proof. |
513 |
513 |
514 \point{How can I tell whether a suggested proof is sound?} |
514 \point{How can I tell whether a suggested proof is sound?} |
515 |
515 |
516 Earlier versions of Sledgehammer often suggested unsound proofs---either proofs |
516 Earlier versions of Sledgehammer often suggested unsound proofs---either proofs |
721 \qty{options} are a list of key--value pairs of the form ``[$k_1 = v_1, |
721 \qty{options} are a list of key--value pairs of the form ``[$k_1 = v_1, |
722 \ldots, k_n = v_n$]''. For Boolean options, ``= \textit{true\/}'' is optional. For |
722 \ldots, k_n = v_n$]''. For Boolean options, ``= \textit{true\/}'' is optional. For |
723 example: |
723 example: |
724 |
724 |
725 \prew |
725 \prew |
726 \textbf{sledgehammer} [\textit{isar\_proof}, \,\textit{timeout} = 120] |
726 \textbf{sledgehammer} [\textit{isar\_proofs}, \,\textit{timeout} = 120] |
727 \postw |
727 \postw |
728 |
728 |
729 Default values can be set using \textbf{sledgehammer\_\allowbreak params}: |
729 Default values can be set using \textbf{sledgehammer\_\allowbreak params}: |
730 |
730 |
731 \prew |
731 \prew |
1291 automatic runs. |
1291 automatic runs. |
1292 |
1292 |
1293 \nopagebreak |
1293 \nopagebreak |
1294 {\small See also \textit{overlord} (\S\ref{mode-of-operation}).} |
1294 {\small See also \textit{overlord} (\S\ref{mode-of-operation}).} |
1295 |
1295 |
1296 \opfalse{isar\_proof}{no\_isar\_proof} |
1296 \opfalse{isar\_proofs}{no\_isar\_proofs} |
1297 Specifies whether Isar proofs should be output in addition to one-liner |
1297 Specifies whether Isar proofs should be output in addition to one-liner |
1298 \textit{metis} proofs. Isar proof construction is still experimental and often |
1298 \textit{metis} proofs. Isar proof construction is still experimental and often |
1299 fails; however, they are usually faster and sometimes more robust than |
1299 fails; however, they are usually faster and sometimes more robust than |
1300 \textit{metis} proofs. |
1300 \textit{metis} proofs. |
1301 |
1301 |
1302 \opdefault{isar\_shrink\_factor}{int}{\upshape 1} |
1302 \opdefault{isar\_shrinkage}{int}{\upshape 10} |
1303 Specifies the granularity of the Isar proof. A value of $n$ indicates that each |
1303 Specifies the granularity of the generated Isar proofs if \textit{isar\_proofs} |
1304 Isar proof step should correspond to a group of up to $n$ consecutive proof |
1304 is enabled. A value of $n$ indicates that each Isar proof step should correspond |
1305 steps in the ATP proof. |
1305 to a group of up to $n$ consecutive proof steps in the ATP proof. |
1306 \end{enum} |
1306 \end{enum} |
1307 |
1307 |
1308 \subsection{Authentication} |
1308 \subsection{Authentication} |
1309 \label{authentication} |
1309 \label{authentication} |
1310 |
1310 |