Alladi Ramakrishnan Hall

Resolution Proof Systems

Anil Shukla

IMSc

A propositional proof system (pps) is a proof system for TAUT. In this talk we investigate a particular pps, "resolution proof system".

We review the first exponential size lower bound for resolution (by Haken).

we review relationships among the three complexity measures of resolution: size, width and space. In particular, the talk includes size-width relation for general and tree-like resolutions (by Ben-sasson and Wigderson), size-space relation for tree-like resolutions (by Esteban and Toran), and width-space relation (by Atserias and Dalmau) for general resolutions.

We review combinatorial characterizations of resolution width (by Atserias and Dalmau) and tree-like resolution space (by Impagliazzo and Pudlak).

Finally, we review tradeoffs between various complexity measures (i.e, size, width and space) for tree-like resolutions (by Ben-Sasson).