## The Resolution proof system

Avi Wigderson

Herbert H. Maass Professor, School of Mathematics

March 22, 2016

The Resolution proof system is perhaps the simplest and most universally used in verification system and automated theorem proving. It was introduced by Davis and Putnam in 1960. The study of its efficiency, both in terms of proof length of natural tautologies and in terms of the complexity of finding short proofs has lead over the decades to a rich understanding which is nonetheless incomplete.