Resolution proofs viewed as automata

This note presents a slightly different view of resolution proofs which the author has not seen presented alsewhere. A proof of unsatisfieability of a (CNF) formula S is viewed as a kind of automaton which, given a truth-assignment f, produces a clause C in S such that f(C) is false.

This view leads to a mild generalisation of resolution proof; it is shown, however, that any generalised proof can be converted to a resolution proof which is at least as short.