一句话：无新变量时 DRAT、SPR、PR 等传播冗余证明系统的复杂度与等价性，并给出 RAT^- 指数下界。
论文研究 SAT 求解中的冗余推理规则 BC、RAT、SPR、PR：从子句集 Γ 推出 Γ∪{C}，虽不保证 Γ 蕴含 C，却保持可满足性。若允许新变量，这些系统均等价于扩展 resolution；本文聚焦禁止新变量的受限系统，并引入更一般的替换冗余 SR。作者区分有删除与无删除版本。关键结果：有删除时 DRAT^-、DSPR^-、DPR^- 等价，并与 DBC^- 等价；无删除时，若 SPR 仅推断短子句，SPR^- 可模拟 PR^-。鸽巢、parity、Tseitin、clique-coloring 等难原理均有小 SPR^- 反驳，SPR^- 还能处理 or-ification、xor-ification 与 index gadget lifting。最后证明 RAT^- 反驳的指数下界，分离 RAT^- 与 DRAT^-、SPR^-。
We study the complexity of a range of propositional proof systems which allow inference rules of the form: from a set of clauses $\Gamma$ derive the set of clauses $\Gamma \cup \{ C \}$ where, due to some syntactic condition, $\Gamma \cup \{ C \}$ is satisfiable if $\Gamma$ is, but where $\Gamma$ does not necessarily imply $C$. These inference rules include BC, RAT, SPR and PR (respectively short for blocked clauses, resolution asymmetric tautologies, subset propagation redundancy and propagation redundancy), which arose from work in satisfiability (SAT) solving. We introduce a new, more general rule SR (substitution redundancy). If the new clause $C$ is allowed to include new variables then the systems based on these rules are all equivalent to extended resolution. We focus on restricted systems that do not allow new variables. The systems with deletion, where we can delete a clause from our set at any time, are denoted DBC${}^-$, DRAT${}^-$, DSPR${}^-$, DPR${}^-$ and DSR${}^-$. The systems without deletion are BC${}^-$, RAT${}^-$, SPR${}^-$, PR${}^-$ and SR${}^-$. With deletion, we show that DRAT${}^-$, DSPR${}^-$ and DPR${}^-$ are equivalent. By earlier work of Kiesl, Rebola-Pardo and Heule, they are also equivalent to DBC${}^-$. Without deletion, we show that SPR${}^-$ can simulate PR${}^-$ provided only short clauses are inferred by SPR inferences. We also show that many of the well-known "hard" principles have small SPR${}^-$ refutations. These include the pigeonhole principle, bit pigeonhole principle, parity principle, Tseitin tautologies and clique-coloring tautologies. SPR${}^-$ can also handle or-fication and xor-ification, and lifting with an index gadget. Our final result is an exponential size lower bound for RAT${}^-$ refutations, giving exponential separations between RAT${}^-$ and both DRAT${}^-$ and SPR${}^-$.