documented Sledgehammer option "induction_rules"
authordesharna
Thu, 08 Jul 2021 17:43:35 +0200
changeset 74203 bec00c7ef8dd
parent 74202 f58108b7a60c
child 74204 57423714c29d
documented Sledgehammer option "induction_rules"
src/Doc/Sledgehammer/document/root.tex
--- a/src/Doc/Sledgehammer/document/root.tex	Thu Jul 08 17:23:01 2021 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex	Thu Jul 08 17:43:35 2021 +0200
@@ -961,6 +961,25 @@
 
 \nopagebreak
 {\small See also \textit{type\_enc} (\S\ref{problem-encoding}).}
+
+\opdefault{induction\_rules}{string}{smart}
+Specifies whether induction rules should be considered as relevant facts.
+The following behaviors are available:
+\begin{enum}
+\item[\labelitemi] \textbf{\textit{include}:}
+Induction rules are considered by the relevance filter.
+
+\item[\labelitemi] \textbf{\textit{exclude}:}
+Induction rules are ignored by the relevance filter.
+
+\item[\labelitemi] \textbf{\textit{instantiated}:}
+Induction rules are instantiated based on the conjecture and then
+considered by the relevance filter.
+
+\item[\labelitemi] \textbf{\textit{smart}:}
+Same as \textit{include} if the prover supports higher-order logic;
+same as \textit{exclude} otherwise.
+\end{enum}
 \end{enum}
 
 
@@ -980,9 +999,9 @@
 defined using an equation $\const{c}~x_1~\ldots~x_n = t$ ($\lambda$-lifting).
 
 \item[\labelitemi] \textbf{\textit{opaque\_lifting}:} Same as
-\textbf{\textit{lifting}}, except that the supercombinators are kept opaque,
-i.e. they are unspecified fresh constants. This effectively disables all
-reasoning under $\lambda$-abstractions.
+\textit{lifting}, except that the supercombinators are kept opaque,
+i.e. they are unspecified fresh constants. This effectively disables
+all reasoning under $\lambda$-abstractions.
 
 \item[\labelitemi] \textbf{\textit{combs}:} Rewrite lambdas to the Curry
 combinators (\comb{I}, \comb{K}, \comb{S}, \comb{B}, \comb{C}). Combinators
@@ -992,8 +1011,8 @@
 resolution.
 
 \item[\labelitemi] \textbf{\textit{opaque\_combs}:} Same as
-\textbf{\textit{combs}}, except that the combinators are kept opaque,
-i.e. without equational definitions.
+\textit{combs}, except that the combinators are kept opaque, i.e. without
+equational definitions.
 
 \item[\labelitemi] \textbf{\textit{combs\_and\_lifting}:} Introduce a new
 supercombinator \const{c} for each cluster of $\lambda$-abstractions and characterize it both using a