ECCC-Report TR21-176https://eccc.weizmann.ac.il/report/2021/176Comments and Revisions published for TR21-176en-usWed, 08 Dec 2021 22:55:22 +0200
Paper TR21-176
| A super-polynomial separation between resolution and cut-free sequent calculus |
Theodoros Papamakarios
https://eccc.weizmann.ac.il/report/2021/176We show a quadratic separation between resolution and cut-free sequent calculus width. We use this gap to get, for the first time, first, a super-polynomial separation between resolution and cut-free sequent calculus for refuting CNF formulas, and secondly, a quadratic separation between resolution width and monomial space in polynomial calculus with resolution. Our super-polynomial separation between resolution and cut-free sequent calculus only applies when clauses are seen as disjunctions of unbounded arity; our examples have linear size cut-free sequent calculus proofs writing, in a particular way, their clauses using binary disjunctions. Interestingly, this shows that the complexity of sequent calculus depends on how disjunctions are represented.Wed, 08 Dec 2021 22:55:22 +0200https://eccc.weizmann.ac.il/report/2021/176