<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=us-ascii">
<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:Aptos;
panose-1:2 11 0 4 2 2 2 2 2 4;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0in;
font-size:11.0pt;
font-family:"Aptos",sans-serif;
mso-ligatures:standardcontextual;}
a:link, span.MsoHyperlink
{mso-style-priority:99;
color:#467886;
text-decoration:underline;}
.MsoChpDefault
{mso-style-type:export-only;
font-size:11.0pt;
mso-ligatures:none;}
@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="#467886" vlink="#96607D" style="word-wrap:break-word">
<div class="WordSection1">
<p class="MsoNormal"><span style="font-family:"Arial",sans-serif">This is an announcement of Theodoros Papamakarios's
<span style="color:#3C4043;letter-spacing:.15pt;background:white">Dissertation Defense</span>.<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-family:"Arial",sans-serif">===============================================<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-family:"Arial",sans-serif">Candidate: Theodoros Papamakarios<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-family:"Arial",sans-serif"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="font-family:"Arial",sans-serif">Date: Tuesday, July 16, 2024<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-family:"Arial",sans-serif"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="font-family:"Arial",sans-serif">Time: 12 pm CST<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-family:"Arial",sans-serif"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="font-family:"Arial",sans-serif">Location: JCL 298<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-family:"Arial",sans-serif"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="font-family:"Arial",sans-serif">Remote Location:
<a href="https://urldefense.com/v3/__https:/uchicago.zoom.us/j/93668031337?pwd=ReNoOlWJObaCZcwRWiMBDG8HILXrya.1__;!!BpyFHLRN4TMTrA!4KH2ezfraDG30JezqhkymUmTtL9FGSoedS4cF9LbGl9moJ3sAwNnQHl1fWq_--PKa5Ps-rLvWYGnGSaT7J8-lQIBeo2xqg$" title="https://urldefense.com/v3/__https:/uchicago.zoom.us/j/93668031337?pwd=ReNoOlWJObaCZcwRWiMBDG8HILXrya.1__;!!BpyFHLRN4TMTrA!4KH2ezfraDG30JezqhkymUmTtL9FGSoedS4cF9LbGl9moJ3sAwNnQHl1fWq_--PKa5Ps-rLvWYGnGSaT7J8-lQIBeo2xqg$">
<span style="color:#0078D7">https://uchicago.zoom.us/j/93668031337?pwd=ReNoOlWJObaCZcwRWiMBDG8HILXrya.1</span></a><span style="color:#212121"><br>
Meeting ID: 936 6803 1337<br>
Passcode: 670693</span><o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-family:"Arial",sans-serif"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="font-family:"Arial",sans-serif">Title: <span style="color:#3C4043;letter-spacing:.15pt;background:white">
Complexity measures, separations, and automatability in proof complexity</span><o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-family:"Arial",sans-serif"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="font-family:"Arial",sans-serif">Abstract: </span>
<span style="font-family:"Arial",sans-serif;color:black;mso-ligatures:none"> With the rise of computer science, questions like "can we solve a problem?'' got a quantitative counterpart: "how hard is it to solve a problem?''. Proof complexity deals with the
quantitative version of "can we prove a theorem?'', namely, the question "how hard is it to prove a theorem?''. The systematic study of the latter question for propositional proof systems. The systematic study of the latter question for propositional proof
systems started with Cook and Reckhow, initiating a line of research which investigates how different proof systems for propositional logic compare with each other with respect to the minimum size needed to prove tautological formulas. A question that had
remained open in the classification of Cook and Reckhow is whether cut-free sequent calculus can polynomially simulate resolution, in other words, whether adding atomic cuts to cut-free sequent calculus can super-polynomially decrease the size of proofs. We
answer this question negatively, by showing a super-polynomial separation between cut-free sequent calculus as a system for refuting sets of clauses, and resolution.</span><span style="font-family:"Arial",sans-serif;color:#212121;mso-ligatures:none"><o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-family:"Arial",sans-serif;color:#212121;mso-ligatures:none"> <o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-family:"Arial",sans-serif;color:black;mso-ligatures:none">Now, while size is certainly the most well studied, and arguably the most important measure of the complexity of proofs, other complexity measures have emerged,
along with a line of study about relations between them, lack of relations thereof, and the inherent impossibility of optimizing two different measures at once. We contribute to this line of research by identifying two new clusters of known proof complexity
measures equal up to polynomial and logn factors. The first cluster contains the logarithm of tree-like resolution size, regularized clause and monomial space, and clause space, ordinary and regularized, in regular and tree-like resolution. Consequently, separating
clause or monomial space from the logarithm of </span><span style="font-family:"Arial",sans-serif;color:#212121;mso-ligatures:none">tree-like</span><span style="font-family:"Arial",sans-serif;color:black;mso-ligatures:none"> resolution size is equivalent to
showing strong trade-offs between clause space and length, and equivalent to showing super-critical trade-offs between clause space and depth. The second cluster contains resolution width, Sigma_2 space (a generalization of clause space to depth-2 Frege systems),
ordinary and regularized, and the logarithm of tree-like R(log) size. As an application, we improve a known size-space trade-off for polynomial calculus with resolution. We further show a quadratic lower bound on tree-like resolution size for formulas refutable
in clause space 4, and introduce a measure intermediate between depth and the logarithm of tree-like resolution size that might be of independent interest.</span><span style="font-family:"Arial",sans-serif;color:#212121;mso-ligatures:none"><o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-family:"Arial",sans-serif;color:#212121;mso-ligatures:none"> <o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-family:"Arial",sans-serif;color:black;mso-ligatures:none">A third contribution of the dissertation is on the topic of automatability, that is the topic of how hard it is to find short proofs of a statement in a proof system.
Significantly refining earlier results, Atserias and Muller showed that the problem of automatability is NP-hard for resolution. Subsequently, this result was extended to stronger proof systems, including cutting planes, Res(k), and algebraic proof systems.
We extend it to bounded-depth Frege, showing that for any d, depth-d Frege systems are NP-hard to automate.</span><span style="font-family:"Arial",sans-serif;color:#212121;mso-ligatures:none"><o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-family:"Arial",sans-serif"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="font-family:"Arial",sans-serif"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="font-family:"Arial",sans-serif">Advisors: Alexander Razborov<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-family:"Arial",sans-serif"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="font-family:"Arial",sans-serif">Committee Members: Aaron Potechin, Alexander Razborov, and Madhur Tulsiani<o:p></o:p></span></p>
<div>
<div>
<p class="MsoNormal"><b><span style="font-family:"Arial",sans-serif;color:black;mso-ligatures:none"><o:p> </o:p></span></b></p>
</div>
</div>
</div>
</body>
</html>