<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=Windows-1252">
<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;}
@font-face
{font-family:"Helvetica Neue";
panose-1:2 0 5 3 0 0 0 2 0 4;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0in;
font-size:11.0pt;
font-family:"Calibri",sans-serif;
mso-ligatures:standardcontextual;}
span.EmailStyle17
{mso-style-type:personal-compose;
font-family:"Calibri",sans-serif;
color:windowtext;}
p.p1, li.p1, div.p1
{mso-style-name:p1;
margin:0in;
font-size:10.0pt;
font-family:"Helvetica Neue";}
p.p2, li.p2, div.p2
{mso-style-name:p2;
margin:0in;
font-size:10.0pt;
font-family:"Helvetica Neue";}
.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="p1">This is an announcement of Theodoros Papamakarios’ Candidacy Exam.<o:p></o:p></p>
<p class="p1">===============================================<o:p></o:p></p>
<p class="p1">Candidate: Theodoros Papamakarios<o:p></o:p></p>
<p class="p2"><o:p> </o:p></p>
<p class="p1">Date: Monday, October 9th,2023<o:p></o:p></p>
<p class="p2"><o:p> </o:p></p>
<p class="p1">Time: 4:00pm CST<o:p></o:p></p>
<p class="p2"><o:p> </o:p></p>
<p class="p1">Location: JCL 390<o:p></o:p></p>
<p class="p2"><o:p> </o:p></p>
<p class="p1">Title: On Automatability<o:p></o:p></p>
<p class="p2"><o:p> </o:p></p>
<p class="p1">Abstract: The problem of proof search is central to automated theorem proving, and has been the driving force behind many theoretical advances: Provided that short proofs of a statement exist, how hard is to find one? More concretely, a proof
system P is called automatable if there is an algorithm that, given a formula F, finds a P-proof of F in time polynomial in the size of the shortest P-proof of F. In this presentation, I will start by surveying the role of the notion of automatability in proof
complexity, in particular how it connects to other important threads (e.g. feasible interpolation, canonical pairs). I will then focus on recent non-automatability results for weak propositional proof systems. <o:p></o:p></p>
<p class="p2"><o:p> </o:p></p>
<p class="p1">Advisors: Alexander Razborov<o:p></o:p></p>
<p class="p2"><o:p> </o:p></p>
<p class="p1">Committee Members: Aaron Potechin, Alexander Razborov, and Madhur Tulsiani<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
</body>
</html>