问题描述
在阅读使用SMT求解器扩展大锤时，我阅读以下内容：
在原始的Sledgehammer体系结构中，可用的引理被重写 在调用相关性过滤器之前，使用幼稚的分配定律应用to子句规范形式。为了避免在每次调用时产生数千个引理，这些子句被保留在缓存中。该设计在技术上与（不识别缓存的）smt方法不兼容，并且对于包括自定义多项式时间子句的ATP来说已经不令人满意。
到目前为止，我对SMT的理解如下：SMT不能处理子句。相反，他们尝试为问题的无量词部分建立模型。通过根据一组有效项实例化量词来完善搜索。因此，对于SMT求解器，实际上不需要任何子句形式。
我们重新编写了相关性过滤器，以便对任意HOL公式进行操作，以尝试模拟旧的行为。为了模拟基于子句的代码中与Skolem函数相关的惩罚，我们跟踪极性并检测引起Skolem函数的量词。
与Skolem函数相关的惩罚是什么？我可以理解它们对SMT不利，但在这里看来它们对ATP也不利...
解决方法
首先，SMT求解程序对子句进行处理，并且内部肯定存在一些（非幼稚的）规范化（例如，最小作用域）。但是您不需要在调用SMT求解器之前进行规范化（特别是因为它会更幼稚并生成更多子句）。
无论如何，Section 6.6.7 explains why skolemization was done on the Isabelle side。综上所述：在Isabelle的证明中不可能引入多态常数。因此必须在开始证明之前完成。
在撰写论文时，不更改过滤条件似乎会导致性能变差，因此增加了罚款。但是，我试图在Sledgehammer中找到相关的模拟clausification的代码，所以我不认为这种情况会发生。