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.