Resolution Proofs of Matching Principles

This paper discusses current techniques for proving lower bounds on the size of resolution proofs from sets of clauses expressing assertions about matchings in bipartite graphs (a class including the well-known pigeon-hole clauses). The techniques are illustrated by demonstrating an improved lower bound for some examples discussed by Kleine Büning. The final section discusses some problems where current techniques appear inadequate, and new ideas seem to be required.