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.

翻译：计算的局部化在高效求解困难问题中扮演着关键角色。我们将实现这种局部化的技术称为${\mathit 局部}$${\mathit 计算}$。本文建立了局部计算与$\mathit{部分量词消去}$（PQE）之间的联系。后者是常规量词消去的推广，允许将公式的$\mathit{部分}$子式移出量词作用域之外。本文旨在论证PQE可被视为局部计算的语言，因此构建高效的PQE求解器具有重要意义。我们描述了通过PQE实现局部计算在硬件验证中三个不同问题上的应用：性质生成、等价性检验和模型检验。此外，还讨论了利用PQE进行局部计算在SAT求解中的应用。最后，我们建立了PQE与插值（一种局部计算形式）之间的关联。