大锤如何将lambda-抽象转换为ATP？

问题描述

在带有SMT求解器的扩展大锤中有这样的说法：

Lambda抽象将重写为Turner组合器，或者使用Lambda抽象将其转换为显式函数。

链接的引用将高阶子句转换为一阶子句并未阐明此方法如何同步。我们是否总是同时使用它们？是一个比另一个更好的吗？

解决方法

根据mediatum.ub.tum.de/doc/1097834/1097834.pdf为每个证明者量身定制方法。