The width complexity measure plays a central role in Resolution and other propositional proof systems like Polynomial Calculus (under the name of degree). The study of width lower bounds is the most extended method for proving size lower bounds, and it is known that for these systems, proofs with small ... more >>>

We show that the number of variables and the quantifier depth needed to distinguish a pair of graphs by first-order logic sentences exactly match the complexity measures of clause width and positive depth needed to refute the corresponding graph isomorphism formula in propositional narrow resolution.

Using this connection, we ... more >>>

We show a new connection between the space measure in tree-like resolution and the reversible pebble game in graphs. Using this connection we provide several formula classes for which there is a logarithmic factor separation between the space complexity measure in tree-like and general resolution. We show that these separations ... more >>>