__Preprint:__

**
Sam Buss and Emre Yolcu
Regular Resoluion Effectively Simulates Resolution
To appear in **

Download preprint version.

**Abstract**
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.