Suppose I wanted to find a proof of the pigeonhole principle or show that no  proof shorter than $L$ exists. I understand that proof-checking is in NP, so I could write a CNF formula that is satisfiable iff. such a proof exists. What I want to know is, how exactly would one do that? I understand I would assume a set of axioms about sets or something and also the axioms of first-order predicate calculus, and probably also modus ponens and stuff... but how exactly does one do something like this? Can anyone give a construction of such a CNF formula? References to papers or general explanations would be appreciated.
How would one prove the pigeonhole principle with a SAT solver?
reference request;logic;satisfiability;first order logic;proof assistants