Localization of computations plays a crucial role in solving hard problems efficiently. We will refer to the techniques implementing such localization as ${\mathit local}$ ${\mathit computing}$. We relate local computing with $\mathit{partial}$ $\mathit{quantifier}$ $\mathit{elimination}$ (PQE). The latter is a generalization of regular quantifier elimination where one can take a $\mathit{part}$ of the formula out of the scope of quantifiers. The objective of this paper is to show that PQE can be viewed as a language of local computing and hence building efficient PQE solvers is of great importance. We describe application of local computing by PQE to three different problems of hardware verification: property generation, equivalence checking and model checking. Besides, we discuss using local computing by PQE for SAT solving. Finally, we relate PQE and interpolation, a form of local computing.

翻译：计算的局部化在高效求解复杂问题中起着关键作用。我们将实现此类局部化的技术称为"局部计算"。我们将局部计算与部分量词消去相关联，后者是常规量词消去的推广形式，允许将公式的一部分移出量词作用域。本文旨在证明部分量词消去可被视为局部计算的一种表述语言，因此构建高效的部分量词消去求解器具有重要价值。我们描述了通过部分量词消去实现局部计算在硬件验证中三个不同问题上的应用：属性生成、等价性检验和模型检验。此外，我们探讨了利用部分量词消去进行SAT求解的局部计算方法。最后，我们建立了部分量词消去与插值（一种局部计算形式）之间的关联。