The complexity of resolution refutations of contradictory sets of clauses in propositional logic has been investigated deeply over the last forty years, beginning with the groundbreaking paper of Tseitin , based on a talk given in a Leningrad seminar of 1966.
A general theme that emerged gradually in the course of the intensive investigations of the last few decades has been that of basing
lower bounds on lower bounds on the
of refutations. Roughly speaking, it turns out that in many cases, the minimum size of a refutation is exponential in the minimum width.