In the implicit version of a propositional proof system Q, we work with Q-proofs that are not written down directly, but are succinctly encoded by circuits. Thus implicit Q-proofs are potentially exponentially shorter than usual Q-proofs. We study narrow implicit proofs, a restricted version of this notion, in which lines in the encoded proof can only have polynomial size. We use a cut-elimination construction to show that G_{i+1} is equivalent to narrow implicit G_i, for i >= 1, where G_i is the extension of Frege allowing reasoning with Sigma^q_i quantified propositional formulas. We show that G_1 is equivalent to implicit resolution.

翻译：在命题证明系统Q的隐式版本中，我们处理并非直接书写、而是通过电路简洁编码的Q-证明。因此隐式Q-证明在长度上可能比通常的Q-证明指数级更短。我们研究此概念的受限版本——狭窄隐式证明，其中编码证明中的行仅能具有多项式规模。我们利用切割消去构造证明：对于 i ≥ 1，G_{i+1} 等价于狭窄隐式 G_i，其中 G_i 是允许使用 Sigma^q_i 量化命题公式推理的弗雷格系统的扩展。我们证明 G_1 等价于隐式归结法。