SMT和ATPs中的Skolem函数

Question

在使用SMT解决器阅读扩展Sledge锤时，我阅读了以下内容：

在原有的分类器体系结构中，在调用关联过滤器之前，使用分布律的简单应用将可用引理重写为子句范式。为了避免每次调用都会产生数千个引理，子句被保存在缓存中。这种设计在技术上与(缓存不知情的) smt方法不兼容，而且它已经不能满足ATP的要求，其中包括自定义的多项式时间clausifier。

到目前为止，我对SMT的理解如下:SMT不适用于子句。相反，他们试图为问题的无量词部分建立一个模型。搜索是通过实例化量词，根据一组活动术语来改进的。因此，SMT求解器实际上不需要分句形式。

我们重写了关联过滤器，使其操作于任意的HOL公式，试图模拟旧的行为。为了模拟基于子句的代码中与Skolem函数相关的惩罚，我们跟踪极性并检测产生Skolem函数的量词。

与Skolem函数相关的惩罚是什么？我能理解它们对SMTs没有好处，但在这里看来它们对ATP也是不好的。

Answer 1

首先，SMT解决者确实会在子句上工作，并且肯定有一些(非天真的)内部正常化(例如，微小的)。但是您不需要在调用SMT解决程序之前进行规范化(特别是因为它将更加天真，并会生成更多的子句)。

不管怎样，第6.6.7节解释了为什么在伊莎贝尔一侧进行骷髅化。总之:在Isabelle中不可能在证明中引入多态常数，因此必须在开始验证之前完成。

看来，在撰写论文时，不改变过滤可能会导致性能更差，因此增加了惩罚。但是，我试图在Sledge锤中找到相关的代码来模拟clausification，所以我不相信这种情况还会发生。