<html>

<head>

<meta http-equiv="Content-Type" content="text/html; charset=us-ascii">

</head>

<body>

<div class="" style="word-wrap:break-word; line-break:after-white-space">This is an announcement of Theodoros Papamakarios's MS Presentation<br class="">

===============================================<br class="">

Candidate: Theodoros Papamakarios<br class="">

<br class="">

Date: Friday, February 04, 2022<br class="">

<br class="">

Time:  3 pm CST<br class="">

<br class="">

Remote Location:  <a href="https://uchicago.zoom.us/j/94716835621?pwd=OG43V2NYanp4TWhYMWNRK0MrYjVVQT09" class="">https://uchicago.zoom.us/j/94716835621?pwd=OG43V2NYanp4TWhYMWNRK0MrYjVVQT09</a><br class="">

<br class="">

M.S. Paper Title: Separations and characterizations in weak propositional proof systems<br class="">

<br class="">

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.<br class="">

<br class="">

Advisors: Alexander Razborov<br class="">

<br class="">

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

<div class=""><br class="">

</div>

<div class=""></div>

</div>

<div class="" style="word-wrap:break-word; line-break:after-white-space">

<div class=""></div>

</div>

</body>

</html>