[Colloquium] Theodoros Papamakarios MS Presentation/Feb 4, 2022

[Megan Woodward]

This is an announcement of Theodoros Papamakarios's MS Presentation
===============================================
Candidate: Theodoros Papamakarios

Date: Friday, February 04, 2022

Time:  3 pm CST

Remote Location:  https://uchicago.zoom.us/j/94716835621?pwd=OG43V2NYanp4TWhYMWNRK0MrYjVVQT09

M.S. Paper Title: Separations and characterizations in weak propositional proof systems

Abstract: We study weak propositional proof systems as subsystems of sequent calculus. It is well known that allowing more formulas to participate in applications of the cut rule, one gets a hierarchy of systems strictly increasing in strength. We extend this hierarchy at the very bottom to show that even allowing only propositional variables as cuts, one gets a super-polynomially more powerful system. In more customary terms, we show a super-polynomial separation between cut-free sequent calculus and resolution. Furthermore, we identify two new big clusters of proof complexity measures equivalent up to polynomial and $\log n$ factors, in the vicinity of the first levels of the above hierarchy. The first cluster contains, among others, the logarithm of tree-like resolution size, regularized (that is, multiplied by the logarithm of proof length) clause and monomial space, and clause space, both ordinary and regularized, in regular and tree-like resolution. As a consequence, separating clause or monomial space from the (logarithm of) tree-like resolution size is the same as showing a strong trade-off between clause or monomial space and proof length, and is the same as showing a super-critical trade-off between clause space and depth. The second cluster contains width, $\Sigma_2$ space (a generalization of clause space to depth 2 Frege systems), both ordinary and regularized, as well as the logarithm of tree-like size in the system $R(\log)$. As an application of some of these simulations, we improve a known size-space trade-off for polynomial calculus with resolution. In terms of separations between the measures above, to show our super-polynomial separation of resolution and cut-free sequent calculus, we show as a first step, a quadratic gap between resolution and cut-free sequent calculus width. This also allows us to get, for the first time, a quadratic separation between resolution width and monomial space in polynomial calculus with resolution. Furthermore, we show a quadratic lower bound on tree-like resolution size for formulas refutable in clause space $4$. We introduce on our way yet another proof complexity measure intermediate between depth and the logarithm of tree-like size in resolution that might be of independent interest.

Advisors: Alexander Razborov

Committee Members: Alexander Razborov, Madhur Tulsiani, and Aaron Potechin

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mailman.cs.uchicago.edu/pipermail/colloquium/attachments/20220203/fe6c5bb7/attachment-0001.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: mthesis.pdf
Type: application/pdf
Size: 428737 bytes
Desc: mthesis.pdf
URL: <http://mailman.cs.uchicago.edu/pipermail/colloquium/attachments/20220203/fe6c5bb7/attachment-0001.pdf>