论文标题
SAT启发的高阶消除
SAT-Inspired Higher-Order Eliminations
论文作者
论文摘要
我们将几种命题预处理技术概括为基于现有的一阶概括的高阶逻辑。这些技术从问题中消除了文字，子句或谓词符号，目的是使其更适合自动证明搜索。我们还介绍了一种新技术，我们称之为Quasipure Fliteral Ountination，严格归入了纯粹的文字消除。新技术在ZipperPosition Theorem Prover中实现。我们的评估表明，它们有时有助于证明源自Isabelle形式化和TPTP库的问题。
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.
