Skolem 在 SMT 和 ATP 中的功能
Skolem functions in SMT and ATPs
在阅读 Extending Sledgehammer with SMT solvers 时，我阅读了以下内容：
In the original Sledgehammer architecture, the available lemmas were rewritten
to clause normal form using a naive application of distributive laws before the relevance filter was invoked. To avoid clausifying thousands of lemmas on each invocation, the clauses were kept in a cache. This design was technically incompatible with the (cache-unaware) smt method, and it was already unsatisfactory for ATPs, which include custom polynomial-time clausifiers.
到目前为止，我对 SMT 的理解如下：SMT 不处理从句。相反，他们尝试为问题的无量词部分建立模型。通过根据一些活动术语集实例化量词来改进搜索。因此，SMT 求解器确实不需要子句形式。
We rewrote the relevance filter so that it operates on arbitrary HOL formulas, trying to simulate the old behavior. To mimic the penalty associated with Skolem functions in the clause-based code, we keep track of polarities and detect quantifiers that give rise to Skolem functions.
与 Skolem 函数相关的惩罚是什么？我可以理解它们对 SMT 不利，但在这里似乎它们对 ATP 也不利...
首先，SMT 求解器会处理子句，并且内部肯定有一些 (non-naive) 规范化（例如，缩小范围）。但是您不需要在调用 SMT 求解器之前进行归一化（特别是，因为它会更天真并生成更多的子句）。
无论如何，Section 6.6.7 explains why skolemization was done on the Isabelle side。总结一下：在 Isabelle 的证明中不可能引入多态常量；因此必须在开始证明之前完成。
似乎在撰写论文时，不更改过滤会导致性能下降，因此增加了惩罚。但是，我试图在Sledgehammer中找到相关的模拟瘫痪的代码，所以我不相信这种情况会发生。
在阅读 Extending Sledgehammer with SMT solvers 时，我阅读了以下内容：
In the original Sledgehammer architecture, the available lemmas were rewritten to clause normal form using a naive application of distributive laws before the relevance filter was invoked. To avoid clausifying thousands of lemmas on each invocation, the clauses were kept in a cache. This design was technically incompatible with the (cache-unaware) smt method, and it was already unsatisfactory for ATPs, which include custom polynomial-time clausifiers.
到目前为止，我对 SMT 的理解如下：SMT 不处理从句。相反，他们尝试为问题的无量词部分建立模型。通过根据一些活动术语集实例化量词来改进搜索。因此，SMT 求解器确实不需要子句形式。
We rewrote the relevance filter so that it operates on arbitrary HOL formulas, trying to simulate the old behavior. To mimic the penalty associated with Skolem functions in the clause-based code, we keep track of polarities and detect quantifiers that give rise to Skolem functions.
与 Skolem 函数相关的惩罚是什么？我可以理解它们对 SMT 不利，但在这里似乎它们对 ATP 也不利...
首先，SMT 求解器会处理子句，并且内部肯定有一些 (non-naive) 规范化（例如，缩小范围）。但是您不需要在调用 SMT 求解器之前进行归一化（特别是，因为它会更天真并生成更多的子句）。
无论如何，Section 6.6.7 explains why skolemization was done on the Isabelle side。总结一下：在 Isabelle 的证明中不可能引入多态常量；因此必须在开始证明之前完成。
似乎在撰写论文时，不更改过滤会导致性能下降，因此增加了惩罚。但是，我试图在Sledgehammer中找到相关的模拟瘫痪的代码，所以我不相信这种情况会发生。