一句话：将多种命题预处理消去技术推广到高阶逻辑，提出拟纯文字消去，并在 Zipperposition 中提升自动证明搜索。
本文研究如何简化高阶逻辑问题以利于自动定理证明。作者从 SAT 预处理思想出发，在已有的一阶推广基础上，将消去文字、子句或谓词符号的若干技术提升到高阶逻辑，并提出新的拟纯文字消去（quasipure literal elimination），后者严格包含传统的纯文字消去。所有技术均在 Zipperposition 定理证明器中实现。在来自 Isabelle 形式化和 TPTP 库的问题上评估表明，这些消去技术有时能帮助证明器成功证明目标，说明 SAT 启发的预处理在高阶自动定理证明中具有实用价值。
We generalize several propositional preprocessing techniques to higher-order logic, building on existing first-order generalizations. These techniques eliminate literals, clauses, or predicate symbols from the problem, with the aim of making it more amenable to automatic proof search. We also introduce a new technique, which we call quasipure literal elimination, that strictly subsumes pure literal elimination. The new techniques are implemented in the Zipperposition theorem prover. Our evaluation shows that they sometimes help prove problems originating from Isabelle formalizations and the TPTP library.