The importance of {\em width} as a resource in resolution theorem proving
has been emphasized in work of Ben-Sasson and Wigderson. Their results show that lower
bounds on the size of resolution refutations can be proved in a uniform manner by
demonstrating lower bounds on the width of refutations, and that there is a simple
dynamic programming procedure for automated theorem proving, based on the search for
small width proofs. The present article shows that the problem of determining, given
a set of clauses Sigma and an integer k, whether Sigma has a refutation of width k,
is EXPTIME-complete. The proof is by a reduction from the Existential k-pebble game,
proved EXPTIME-complete by Kolaitis and Panttaja.