445 |
445 |
446 \subsection{Relevance Filter} |
446 \subsection{Relevance Filter} |
447 \label{relevance-filter} |
447 \label{relevance-filter} |
448 |
448 |
449 \begin{enum} |
449 \begin{enum} |
450 \opdefault{relevance\_threshold}{int}{40} |
450 \opdefault{relevance\_thresholds}{int\_pair}{45~95} |
451 Specifies the threshold above which facts are considered relevant by the |
451 Specifies the thresholds above which facts are considered relevant by the |
452 relevance filter. The option ranges from 0 to 100, where 0 means that all |
452 relevance filter. The first threshold is used for the first iteration of the |
453 theorems are relevant. |
453 relevance filter and the second threshold is used for the last iteration (if it |
454 |
454 is reached). The effective threshold is quadratically interpolated for the other |
455 \opdefault{relevance\_decay}{int}{31} |
455 iterations. Each threshold ranges from 0 to 100, where 0 means that all theorems |
456 Specifies the decay factor, expressed as a percentage, used by the relevance |
456 are relevant and 100 only theorems that refer to previously seen constants. |
457 filter. This factor is used by the relevance filter to scale down the relevance |
457 |
458 of new facts at each iteration of the filter. |
458 \opdefault{max\_relevant}{int\_or\_smart}{\textit{smart}} |
459 |
459 Specifies the maximum number of facts that may be returned by the relevance |
460 \opdefault{max\_relevant\_per\_iter}{int\_or\_smart}{\textit{smart}} |
460 filter. If the option is set to \textit{smart}, it is set to a value that was |
461 Specifies the maximum number of facts that may be added during one iteration of |
461 empirically found to be appropriate for the ATP. A typical value would be 300. |
462 the relevance filter. If the option is set to \textit{smart}, it is set to a |
|
463 value that was empirically found to be appropriate for the ATP. A typical value |
|
464 would be 50. |
|
465 |
462 |
466 \opsmartx{theory\_relevant}{theory\_irrelevant} |
463 \opsmartx{theory\_relevant}{theory\_irrelevant} |
467 Specifies whether the theory from which a fact comes should be taken into |
464 Specifies whether the theory from which a fact comes should be taken into |
468 consideration by the relevance filter. If the option is set to \textit{smart}, |
465 consideration by the relevance filter. If the option is set to \textit{smart}, |
469 it is taken to be \textit{true} for SPASS and \textit{false} for E and Vampire, |
466 it is taken to be \textit{true} for SPASS and \textit{false} for the other ATPs; |
470 because empirical results suggest that these are the best settings. |
467 empirical results suggest that these are the best settings. |
471 |
468 |
472 %\opfalse{defs\_relevant}{defs\_irrelevant} |
469 %\opfalse{defs\_relevant}{defs\_irrelevant} |
473 %Specifies whether the definition of constants occurring in the formula to prove |
470 %Specifies whether the definition of constants occurring in the formula to prove |
474 %should be considered particularly relevant. Enabling this option tends to lead |
471 %should be considered particularly relevant. Enabling this option tends to lead |
475 %to larger problems and typically slows down the ATPs. |
472 %to larger problems and typically slows down the ATPs. |
476 |
|
477 \end{enum} |
473 \end{enum} |
478 |
474 |
479 \subsection{Output Format} |
475 \subsection{Output Format} |
480 \label{output-format} |
476 \label{output-format} |
481 |
477 |