Abstract
Joanna Ochremiak
Title: Proof Complexity meets Finite Model Theory
Abstract: Finite model theory (FMT) is the study of the expressive power of logics on the class of all finite structures. In this talk I will discuss connections between FMT and proof complexity. After a short introduction and an overview of selected results I will focus on joint work with Albert Atserias on the power of the Sherali-Adams, Sums-of-Squares and Polynomial Calculus proof systems for the graph isomorphism problem. I will present results concerning the relative strength of those proof systems via an excursion into the descriptive complexity of the ellipsoid method, and bounded-variable infinitary logics.
Robert Robere
Title: Hard Formulas in Proof Complexity by Composition
Abstract: In propositional proof complexity, one of the central tools in constructing formulas that are hard to refute is composition. For a simple example: if we have a CNF formula F, we can replace each variable x in F with another small boolean function (say, the XOR of two fresh variables), and then re-write this new substituted formula into CNF. These techniques are informally referred to as lifting theorems, and they have deep connections with areas in complexity theory like circuit complexity and communication complexity. In this talk, we give a gentle introduction to lifting results in proof complexity, and outline some of the ways lifting can be used to control various "proof complexity parameters" of unsatisfiable CNF formulas (like proof length, proof space, proof depth, etc.).
Susanna de Rezende
Title: Non-Automatability: When Finding Proofs Is Provably Hard
Abstract: The proof search problem is a central question in automated theorem proving and SAT solving. Clearly, if a propositional tautology F does not have a short (polynomial size) proof in a proof system P, any algorithm that searches for P-proofs of F will necessarily take super-polynomial time. But can proofs of "easy" formulas, i.e., those that have polynomial size proofs, be found in polynomial time? This question motivates the study of automatability of proof systems. In this talk, we give an overview of known non-automatability results, focusing on the more recent ones, and present the main ideas used to obtain them.