[Proof Complexity] Seminar on Monday - Theodoros Papamakarios

[thapen]

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