We study propositional proof systems with inference rules that formalize restricted versions of the ability to make assumptions that hold without loss of generality, commonly used informally to shorten proofs. Each system we study is built on resolution. They are called BC${}^-$, RAT${}^-$, SBC${}^-$, and GER${}^-$, denoting respectively blocked clauses, resolution asymmetric tautologies, set-blocked clauses, and generalized extended resolution - all "without new variables." They may be viewed as weak versions of extended resolution (ER) since they are defined by first generalizing the extension rule and then taking away the ability to introduce new variables. Except for SBC${}^-$, they are known to be strictly between resolution and extended resolution. Several separations between these systems were proved earlier by exploiting the fact that they effectively simulate ER. We answer the questions left open: We prove exponential lower bounds for SBC${}^-$ proofs of a binary encoding of the pigeonhole principle, which separates ER from SBC${}^-$. Using this new separation, we prove that both RAT${}^-$ and GER${}^-$ are exponentially separated from SBC${}^-$. This completes the picture of their relative strengths.

翻译：我们研究命题证明系统中的推理规则，这些规则形式化了“可无损假设成立”能力的受限版本——这种能力在非形式化证明中常被用于缩短论证。我们研究的每个系统均基于归结原理构建，分别称为BC${}^-$（阻塞子句）、RAT${}^-$（归结非对称重言式）、SBC${}^-$（集合阻塞子句）和GER${}^-$（广义扩展归结），其共同特征为“不含新变量”。这些系统可视为扩展归结（ER）的弱化版本：通过先推广扩展规则，再移除引入新变量的能力而定义。除SBC${}^-$外，已知其余系统严格介于归结与扩展归结之间。先前的研究通过利用这些系统可有效模拟ER的事实，证明了它们之间的若干分离关系。我们解决了遗留的公开问题：针对鸽巢原理的二进制编码，证明了SBC${}^-$证明的指数下界，从而将ER与SBC${}^-$分离。利用这一新的分离结果，我们进一步证明RAT${}^-$和GER${}^-$均与SBC${}^-$呈指数分离。这完整揭示了这些系统的相对证明强度图景。