Proofs in propositional logic are typically presented as trees of derived formulas or, alternatively, as directed acyclic graphs of derived formulas. This distinction between tree-like vs. dag-like structure is particularly relevant when making quantitative considerations regarding, for example, proof size. Here we analyze a more general type of structural restriction for proofs in rule-based proof systems. In this definition, proofs are directed graphs of derived formulas in which cycles are allowed as long as every formula is derived at least as many times as it is required as a premise. We call such proofs "circular". We show that, for all sets of standard inference rules with single or multiple conclusions, circular proofs are sound. We start the study of the proof complexity of circular proofs at Circular Resolution, the circular version of Resolution. We immediately see that Circular Resolution is stronger than Dag-like Resolution since, as we show, the propositional encoding of the pigeonhole principle has circular Resolution proofs of polynomial size. Furthermore, for derivations of clauses from clauses, we show that Circular Resolution is, surprisingly, equivalent to Sherali-Adams, a proof system for reasoning through polynomial inequalities that has linear programming at its base. As corollaries we get: 1) polynomial-time (LP-based) algorithms that find Circular Resolution proofs of constant width, 2) examples that separate Circular from Dag-like Resolution, such as the pigeonhole principle and its variants, and 3) exponentially hard cases for Circular Resolution. Contrary to the case of Circular Resolution, for Frege we show that circular proofs can be converted into tree-like proofs with at most polynomial overhead.

翻译：命题逻辑中的证明通常以推导公式的树状结构呈现，或者等价地以推导公式的有向无环图结构呈现。这种树状结构与有向无环图结构之间的区分，在涉及证明规模等定量考量时尤为关键。本文分析基于规则的证明系统中一种更具一般性的证明结构限制类型。在这种定义下，证明被表示为推导公式的有向图，其中允许存在循环，只要每个公式被推导的次数至少等于其作为前提被需要的次数。我们将此类证明称为"循环证明"。我们证明，对于所有具有单结论或多结论的标准推理规则集，循环证明都是合理的。我们以循环消解（Circular Resolution）——即消解规则的循环版本——为起点，开始研究循环证明的证明复杂性。我们立即发现，循环消解比有向无环图消解更强，因为如我们所展示，鸽笼原理的命题编码具有多项式规模的循环消解证明。此外，对于从句推导子句的情况，我们惊奇地发现，循环消解等价于Sherali-Adams——一种基于线性规划通过多项式不等式进行推理的证明系统。作为推论，我们得到：1）基于线性规划的多项式时间算法，可寻找常数宽度的循环消解证明；2）区分循环消解与有向无环图消解的实例，例如鸽笼原理及其变体；3）循环消解的指数级困难案例。与循环消解的情况相反，对于弗雷格系统，我们证明循环证明至多可以通过多项式开销转化为树状证明。