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库产生的问题。