Proof Complexity - Automatizability

Automatizability

A proof method is automatizable if one of the shorter proofs of a formula can always be generated in time polynomial (or sub-exponential) in the size of the proof. Some methods, but not all, are automatizable. Automatizability results are not in contrast with the assumption that the polynomial hierarchy does not collapses, which would happen if generating a proof in time polynomial in the size of the formula were always possible.