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.

翻译：我们将若干命题逻辑预处理技术推广至高阶逻辑，并基于已有的—阶逻辑推广方法。这些技术从问题中消去文字、子句或谓词符号，旨在使其更适用于自动证明搜索。我们还引入了一种称为准纯文字消去的新技术，该技术严格包含了纯文字消去方法。这些新技术已在Zipperposition定理证明器中实现。实验评估表明，它们有时能帮助证明源自Isabelle形式化及TPTP库的问题。