Plenary Talk
Automating Resolution is NP-hard
On-site
Together with Albert Atserias we showed that it is NP-hard to find a Resolution refutation that is at most polynomially longer than a shortest one. The talk presents this result in its historical context.
This document was translated from LATEX by HEVEA.