<html xmlns:o="urn:schemas-microsoft-com:office:office" xmlns:w="urn:schemas-microsoft-com:office:word" xmlns:m="http://schemas.microsoft.com/office/2004/12/omml" xmlns="http://www.w3.org/TR/REC-html40">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<meta name="Generator" content="Microsoft Word 15 (filtered medium)">
<style><!--
/* Font Definitions */
@font-face
{font-family:"Cambria Math";
panose-1:2 4 5 3 5 4 6 3 2 4;}
@font-face
{font-family:Calibri;
panose-1:2 15 5 2 2 2 4 3 2 4;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0in;
font-size:11.0pt;
font-family:"Calibri",sans-serif;}
a:link, span.MsoHyperlink
{mso-style-priority:99;
color:#0563C1;
text-decoration:underline;}
span.EmailStyle17
{mso-style-type:personal-compose;
font-family:"Calibri",sans-serif;
color:windowtext;}
span.apple-converted-space
{mso-style-name:apple-converted-space;}
.MsoChpDefault
{mso-style-type:export-only;
font-family:"Calibri",sans-serif;}
@page WordSection1
{size:8.5in 11.0in;
margin:1.0in 1.0in 1.0in 1.0in;}
div.WordSection1
{page:WordSection1;}
--></style>
</head>
<body lang="EN-US" link="#0563C1" vlink="#954F72" style="word-wrap:break-word">
<div class="WordSection1">
<p class="MsoNormal"><span style="font-size:10.5pt;color:black">This is an announcement of Theodoros Papamakarios's MS Presentation<br>
===============================================<br>
Candidate: Theodoros Papamakarios<br>
<br>
Date: Friday, February 04, 2022<br>
<br>
Time: 3 pm CST<br>
<br>
Remote Location: </span><a href="https://uchicago.zoom.us/j/94716835621?pwd=OG43V2NYanp4TWhYMWNRK0MrYjVVQT09" title="https://uchicago.zoom.us/j/94716835621?pwd=OG43V2NYanp4TWhYMWNRK0MrYjVVQT09"><span style="font-size:10.5pt">https://uchicago.zoom.us/j/94716835621?pwd=OG43V2NYanp4TWhYMWNRK0MrYjVVQT09</span></a><span style="font-size:10.5pt;color:black"><br>
<br>
M.S. Paper Title: Separations and characterizations in weak propositional proof systems<br>
<br>
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>
<br>
Advisors: Alexander Razborov<br>
<br>
Committee Members: Alexander Razborov, Madhur Tulsiani, and Aaron Potechin<span class="apple-converted-space"> </span></span><o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
</body>
</html>