doc-src/Sledgehammer/sledgehammer.tex

 \postw
 
 for a successful \textit{metis} proof, you can advantageously pass the
 \textit{full\_types} option to \textit{metis} directly.
 
-\point{And what are the \textit{lam\_lifting} and \textit{hide\_lams} arguments
+\point{And what are the \textit{lifting} and \textit{hide\_lams} arguments
 to Metis?}
 
 Orthogonally to the encoding of types, it is important to choose an appropriate
 translation of $\lambda$-abstractions. Metis supports three translation schemes,
 in decreasing order of power: Curry combinators (the default),

 option (\S\ref{problem-encoding}) and at most one type encoding specification
 with the same semantics as Sledgehammer's \textit{type\_enc} option
 (\S\ref{problem-encoding}).
 %
 The supported $\lambda$ translation schemes are \textit{hide\_lams},
-\textit{lam\_lifting}, and \textit{combinators} (the default).
+\textit{lifting}, and \textit{combs} (the default).
 %
 All the untyped type encodings listed in \S\ref{problem-encoding} are supported.
 For convenience, the following aliases are provided:
 \begin{enum}
 \item[\labelitemi] \textbf{\textit{full\_types}:} Synonym for \textit{poly\_guards\_query}.

 \begin{enum}
 \item[\labelitemi] \textbf{\textit{hide\_lams}:} Hide the $\lambda$-abstractions
 by replacing them by unspecified fresh constants, effectively disabling all
 reasoning under $\lambda$-abstractions.
 
-\item[\labelitemi] \textbf{\textit{lam\_lifting}:} Introduce a new
+\item[\labelitemi] \textbf{\textit{lifting}:} Introduce a new
 supercombinator \const{c} for each cluster of $n$~$\lambda$-abstractions,
 defined using an equation $\const{c}~x_1~\ldots~x_n = t$ ($\lambda$-lifting).
 
-\item[\labelitemi] \textbf{\textit{combinators}:} Rewrite lambdas to the Curry
+\item[\labelitemi] \textbf{\textit{combs}:} Rewrite lambdas to the Curry
 combinators (\comb{I}, \comb{K}, \comb{S}, \comb{B}, \comb{C}). Combinators
 enable the ATPs to synthesize $\lambda$-terms but tend to yield bulkier formulas
 than $\lambda$-lifting: The translation is quadratic in the worst case, and the
 equational definitions of the combinators are very prolific in the context of
 resolution.
 
-\item[\labelitemi] \textbf{\textit{hybrid\_lams}:} Introduce a new
+\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
 lifted equation $\const{c}~x_1~\ldots~x_n = t$ and via Curry combinators.
+
+\item[\labelitemi] \textbf{\textit{combs\_or\_lifting}:} For each cluster of
+$\lambda$-abstractions, heuristically choose between $\lambda$-lifting and Curry
+combinators.
 
 \item[\labelitemi] \textbf{\textit{keep\_lams}:}
 Keep the $\lambda$-abstractions in the generated problems. This is available
 only with provers that support the THF0 syntax.
 
 \item[\labelitemi] \textbf{\textit{smart}:} The actual translation scheme used
 depends on the ATP and should be the most efficient scheme for that ATP.
 \end{enum}
 
-For SMT solvers, the $\lambda$ translation scheme is always
-\textit{lam\_lifting}, irrespective of the value of this option.
+For SMT solvers, the $\lambda$ translation scheme is always \textit{lifting},
+irrespective of the value of this option.
 
 \opdefault{type\_enc}{string}{smart}
 Specifies the type encoding to use in ATP problems. Some of the type encodings
 are unsound, meaning that they can give rise to spurious proofs
 (unreconstructible using \textit{metis}). The supported type encodings are