  We display an application of the notions of kernelization and data reduction
from parameterized complexity to proof complexity: Specifically, we show that
the existence of data reduction rules for a parameterized problem having (a). a
small-length reduction chain, and (b). small-size (extended) Frege proofs
certifying the soundness of reduction steps implies the existence of
subexponential size (extended) Frege proofs for propositional formalizations of
the given problem.
  We apply our result to infer the existence of subexponential Frege and
extended Frege proofs for a variety of problems. Improving earlier results of
Aisenberg et al. (ICALP 2015), we show that propositional formulas expressing
(a stronger form of) the Kneser-Lov\'asz Theorem have polynomial size Frege
proofs for each constant value of the parameter k. Previously only
quasipolynomial bounds were known (and only for the ordinary Kneser-Lov\'asz
Theorem).
  Another notable application of our framework is to impossibility results in
computational social choice: we show that, for any fixed number of agents,
propositional translations of the Arrow and Gibbard-Satterthwaite impossibility
theorems have subexponential size Frege proofs.
