[Proof Complexity] Seminar on Monday - Theodoros Papamakarios
thapen
thapen at math.cas.cz
Thu Sep 30 08:46:25 CEST 2021
Theodoros Papamakarios will give a proof complexity talk in our online
logic seminar on Monday, at 16:00 Prague time - see the announcement
below.
To join go to
https://cesnet.zoom.us/j/472648284?pwd=ZTlxeHhqWlltR1AzZC9CTHgzZ2tRZz09
Passcode: 017107 (if required)
-------------------------------------------------------------------------
Speaker: Theodoros Papamakarios, University of Chicago
Title: A super-polynomial separation between resolution and cut-free
sequent calculus
Abstract
We show a quadratic separation between resolution and cut-free sequent
calculus width. We use this gap to get, 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.
For more information see the seminar web page at
https://calendar.math.cas.cz/logic-seminar-actual .
_______________________________________________
Logic-seminar mailing list
Logic-seminar at math.cas.cz
https://list.math.cas.cz/listinfo/logic-seminar
More information about the Proof-Complexity
mailing list