Regular resolution is a refinement of the resolution proof system requiring that no variable be resolved on more than once along any path in the proof. It is known that there exist sequences of formulas that require exponential-size proofs in regular resolution while admitting polynomial-size proofs in resolution. Thus, with respect to the usual notion of simulation, regular resolution is separated from resolution. An alternative, and weaker, notion for comparing proof systems is that of an "effective simulation," which allows the translation of the formula along with the proof when moving between proof systems. We prove that regular resolution is equivalent to resolution under effective simulations. As a corollary, we recover in a black-box fashion a recent result on the hardness of automating regular resolution.

翻译：正则消解是消解证明系统的一种细化，要求证明中任何路径上每个变量最多被消解一次。已知存在公式序列在正则消解中需要指数规模证明，而在消解中则有多项式规模证明。因此，按通常的模拟概念，正则消解与消解是分离的。比较证明系统的另一种较弱概念是"有效模拟"，它允许在证明系统间转换时对公式及证明进行翻译。我们证明正则消解在有效模拟下等价于消解。作为推论，我们以黑盒方式恢复了关于正则消解自动化困难性的最新结果。