<html xmlns:v="urn:schemas-microsoft-com:vml" xmlns:o="urn:schemas-microsoft-com:office:office" xmlns:w="urn:schemas-microsoft-com:office:word" xmlns:x="urn:schemas-microsoft-com:office:excel" 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;}
span.EmailStyle17
{mso-style-type:personal-compose;
font-family:"Aptos",sans-serif;
color:windowtext;}
span.apple-converted-space
{mso-style-name:apple-converted-space;}
.MsoChpDefault
{mso-style-type:export-only;
font-size:11.0pt;}
@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;color:#212121">This is a reminder of Theodoros Papamakarios's<span class="apple-converted-space"> </span></span><span style="font-family:"Arial",sans-serif;color:#3C4043;letter-spacing:.15pt;background:white">Dissertation
Defense</span><span style="font-family:"Arial",sans-serif;color:#212121">.</span><span style="color:#212121"><o:p></o:p></span></p>
<p class="MsoNormal" style="caret-color: rgb(33, 33, 33);font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;word-spacing:0px">
<span style="font-family:"Arial",sans-serif;color:#212121">===============================================</span><span style="color:#212121"><o:p></o:p></span></p>
<p class="MsoNormal" style="caret-color: rgb(33, 33, 33);font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;word-spacing:0px">
<span style="font-family:"Arial",sans-serif;color:#212121">Candidate: Theodoros Papamakarios</span><span style="color:#212121"><o:p></o:p></span></p>
<p class="MsoNormal" style="caret-color: rgb(33, 33, 33);font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;word-spacing:0px">
<span style="font-family:"Arial",sans-serif;color:#212121"> </span><span style="color:#212121"><o:p></o:p></span></p>
<p class="MsoNormal" style="caret-color: rgb(33, 33, 33);font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;word-spacing:0px">
<span style="font-family:"Arial",sans-serif;color:#212121">Date: Tuesday, July 16, 2024</span><span style="color:#212121"><o:p></o:p></span></p>
<p class="MsoNormal" style="caret-color: rgb(33, 33, 33);font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;word-spacing:0px">
<span style="font-family:"Arial",sans-serif;color:#212121"> </span><span style="color:#212121"><o:p></o:p></span></p>
<p class="MsoNormal" style="caret-color: rgb(33, 33, 33);font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;word-spacing:0px">
<span style="font-family:"Arial",sans-serif;color:#212121">Time: 12 pm CST</span><span style="color:#212121"><o:p></o:p></span></p>
<p class="MsoNormal" style="caret-color: rgb(33, 33, 33);font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;word-spacing:0px">
<span style="font-family:"Arial",sans-serif;color:#212121"> </span><span style="color:#212121"><o:p></o:p></span></p>
<p class="MsoNormal" style="caret-color: rgb(33, 33, 33);font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;word-spacing:0px">
<span style="font-family:"Arial",sans-serif;color:#212121">Location: JCL 298</span><span style="color:#212121"><o:p></o:p></span></p>
<p class="MsoNormal" style="caret-color: rgb(33, 33, 33);font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;word-spacing:0px">
<span style="font-family:"Arial",sans-serif;color:#212121"> </span><span style="color:#212121"><o:p></o:p></span></p>
<p class="MsoNormal" style="caret-color: rgb(33, 33, 33);font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;word-spacing:0px">
<span style="font-family:"Arial",sans-serif;color:#212121">Remote Location:<span class="apple-converted-space"> </span><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><br>
Meeting ID: 936 6803 1337<br>
Passcode: 670693</span><span style="color:#212121"><o:p></o:p></span></p>
<p class="MsoNormal" style="caret-color: rgb(33, 33, 33);font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;word-spacing:0px">
<span style="font-family:"Arial",sans-serif;color:#212121"> </span><span style="color:#212121"><o:p></o:p></span></p>
<p class="MsoNormal" style="caret-color: rgb(33, 33, 33);font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;word-spacing:0px">
<span style="font-family:"Arial",sans-serif;color:#212121">Title:<span class="apple-converted-space"> </span></span><span style="font-family:"Arial",sans-serif;color:#3C4043;letter-spacing:.15pt;background:white">Complexity measures, separations, and automatability in
proof complexity</span><span style="color:#212121"><o:p></o:p></span></p>
<p class="MsoNormal" style="caret-color: rgb(33, 33, 33);font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;word-spacing:0px">
<span style="font-family:"Arial",sans-serif;color:#212121"> </span><span style="color:#212121"><o:p></o:p></span></p>
<p class="MsoNormal" style="caret-color: rgb(33, 33, 33);font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;word-spacing:0px">
<span style="font-family:"Arial",sans-serif;color:#212121">Abstract:<span class="apple-converted-space"> </span></span><span style="font-family:"Arial",sans-serif;color:black"> 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="color:#212121"><o:p></o:p></span></p>
<p class="MsoNormal" style="caret-color: rgb(33, 33, 33);font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;word-spacing:0px">
<span style="font-family:"Arial",sans-serif;color:#212121"> </span><span style="color:#212121"><o:p></o:p></span></p>
<p class="MsoNormal" style="caret-color: rgb(33, 33, 33);font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;word-spacing:0px">
<span style="font-family:"Arial",sans-serif;color:black">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">tree-like</span><span style="font-family:"Arial",sans-serif;color:black"> 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="color:#212121"><o:p></o:p></span></p>
<p class="MsoNormal" style="caret-color: rgb(33, 33, 33);font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;word-spacing:0px">
<span style="font-family:"Arial",sans-serif;color:#212121"> </span><span style="color:#212121"><o:p></o:p></span></p>
<p class="MsoNormal" style="caret-color: rgb(33, 33, 33);font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;word-spacing:0px">
<span style="font-family:"Arial",sans-serif;color:black">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="color:#212121"><o:p></o:p></span></p>
<p class="MsoNormal" style="caret-color: rgb(33, 33, 33);font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;word-spacing:0px">
<span style="font-family:"Arial",sans-serif;color:#212121"> </span><span style="color:#212121"><o:p></o:p></span></p>
<p class="MsoNormal" style="caret-color: rgb(33, 33, 33);font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;word-spacing:0px">
<span style="font-family:"Arial",sans-serif;color:#212121"> </span><span style="color:#212121"><o:p></o:p></span></p>
<p class="MsoNormal" style="caret-color: rgb(33, 33, 33);font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;word-spacing:0px">
<span style="font-family:"Arial",sans-serif;color:#212121">Advisors: Alexander Razborov</span><span style="color:#212121"><o:p></o:p></span></p>
<p class="MsoNormal" style="caret-color: rgb(33, 33, 33);font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;word-spacing:0px">
<span style="font-family:"Arial",sans-serif;color:#212121"> </span><span style="color:#212121"><o:p></o:p></span></p>
<p class="MsoNormal" style="caret-color: rgb(33, 33, 33);font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;word-spacing:0px">
<span style="font-family:"Arial",sans-serif;color:#212121">Committee Members: Aaron Potechin, Alexander Razborov, and Madhur Tulsiani</span><span style="color:#212121"><o:p></o:p></span></p>
<p class="MsoNormal"><b><span style="font-family:"Arial",sans-serif;color:black"> </span></b><span style="color:#212121"><o:p></o:p></span></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
</body>
</html>