Spider 式策略发现与调度构造中的正则化

为了实现最佳性能，自动定理证明器通常依赖于在给定问题上尝试（顺序或并行）多种证明策略的调度。在本文中，我们报告了一项大规模实验，旨在为 Vampire 证明器发现策略，目标为 TPTP 库的 FOF 片段，并基于 Andrei Voronkov 的 Spider 系统的思想为其构建调度。我们从多个角度考察了这一过程，讨论了为 CASC 竞赛获得强 Vampire 调度的难度（或容易程度），并确立了调度对未见问题的泛化能力预期以及影响这一属性的因素。