ACL2 Seminar, 5/19/2017 Speaker: Benjamin Kiesl Title: On Proofs for SAT and QBF Abstract: In my talk, I give an overview on the work I've done during my four months here at UT. In particular, I present results of two papers. The first paper, which is going to appear in the proceedings of CADE (Conference on Automated Deduction), is called "Short Proofs Without New Variables"; in the paper, we introduce proof systems for propositional logic that generalize the DRAT system. To illustrate the expressiveness of these proof systems, we present polynomial-size proofs for the pigeon hole formulas that do not require the introduction of new variables. This is significant since the pigeon hole formulas are a class of formulas that is known for being "hard to prove." The second paper, which is currently under review for the SAT conference, is called "A Little Blocked Literal Goes a Long Way"; in this paper, we show that the QRAT proof system (a generalization of DRAT to quantified Boolean formulas) can polynomially simulate the so-called long-distance-resolution calculus---a calculus that is well-known for its expressiveness, both in theory and in practice.