Neil Thapen, Institute of Mathematics, AS CR, Czech Republic
Random resolution and approximate counting
Resolution is a propositional proof system that is bad at formalizing arguments involving counting, even approximately. I will discuss some upper and lower bounds on random resolution, which roughly speaking adds to resolution the ability to use any axiom, as long as it is true most of the time. This is partly motivated by a question about a related first-order proof system of bounded arithmetic with approximate counting.