Notes on ground resolution.

These notes aimed to give a new perspective on earlier results about the efficiency of ground resolution. These results were established by the Russian mathematician Tseitin in the late 1960s, and later simplified by Galil and again by Ben-Ari. Those results are limited to `regular ground resolution' alone. Although in the notes the same concrete lower bounds are established only for regular resolution (and a trivial generalisation thereof), much of the intermediate work is not limited to regular resolution proofs.

Specifically, it is shown that certain formulae which are refutable have no `short' regular resolution refutations, i.e., all proofs are of exponential length. (Remark: Haken (1984) showed a superpolynomial lower bound for non-regular ground resolution, and Fouks (1992) generalised Tseitin's results to provide an exponential lower bound.)