We study partial quantifier elimination (PQE) for propositional CNF formulas. In contrast to full quantifier elimination, in PQE, one can limit the set of clauses taken out of the scope of quantifiers to a small subset of target clauses. The appeal of PQE is twofold. First, PQE can be dramatically simpler than full quantifier elimination. Second, PQE provides a language for performing incremental computations. Many verification problems (e.g. equivalence checking and model checking) are inherently incremental and so can be solved in terms of PQE. Our approach is based on deriving clauses depending only on unquantified variables that make the target clauses $\mathit{redundant}$. Proving redundancy of a target clause is done by construction of a "certificate" clause implying the former. We describe a PQE algorithm called $\mathit{START}$ that employs the approach above. To evaluate $\mathit{START}$, we apply it to property generation of a sequential circuit $N$. The goal of property generation is to find a $\mathit{bad}$ property of $N$ proving unreachability of a state that is supposed to be reachable. If $N$ has a bad property, it is buggy. Our experiments with FIFO buffers and HWMCC-13 benchmarks suggest that $\mathit{START}$ can be used for detecting bugs in real-life designs.

翻译：我们研究的是配方 CNF 公式的局部量化除去(PQE) 。 与完全量化除去(PQE) 相比, 在PQE 中, 人们可以将从量化范围范围中取出的一组条款限制在一小部分目标条款。 PQE 的吸引力是双重的。 首先, PQE 可以比完全量化消除简单得多。 第二, PQE 提供一种语言用于进行递增计算。 许多核查问题( 如等值检查和模型检查) 本质上是渐进的, 因而可以用PQE 来解决。 我们的方法只能以未量化的变量为基础。 我们的方法只能依据使目标条款成为目标条款 $\ mathit{redant} 范围的未量化的变量。 目标的冗余是通过构建一个“ 认证” 条款, 意味着前一个“ 认证” 。 我们描述一个使用上述方法的PQE 算法, 称为 $\ mathit{ 。 为了评估 $\ Start $, 我们把它应用到一个直序 roupal $nal 。