One of the starting points of propositional proof complexity is the seminal paper by Cook and Reckhow [6], where they defined propositional proof systems as poly-time computable f...
The proof system G∗ 0 of the quantified propositional calculus corresponds to NC1 , and G∗ 1 corresponds to P, but no formula-based proof system that corresponds log space rea...