我们展示了从参数化复杂度到证明复杂度的核化和数据简化概念的应用:具体地，我们证明了具有(a).一个小长度约简链的参数化问题的数据约简规则的存在性，以及(b)证明约简步骤完备性的小尺寸(扩展)弗雷格证明暗示了该问题命题形式化的次指数尺寸(扩展)弗雷格证明的存在性。
我们将所得结果应用于次指数弗雷格的存在性的推导，并对各种问题进行了弗雷格证明的推广。改进了Aisenberg et al. (ICALP 2015)的早期结果，我们证明了表示Kneser-Lovász定理(一种更强形式)的命题公式对于参数k的每个常值都有多项式大小的Frege证明。以前只有拟多项式的界是已知的(而且只有普通的Kneser-Lovász定理)。
我们的框架的另一个值得注意的应用是计算社会选择中的不可能结果:我们证明，对于任何固定数量的代理，阿罗和吉巴德-萨特思韦特不可能定理的命题平移具有次指数大小的弗雷格证明。
原文题目：Kernelization, Proof Complexity and Social Choice
原文：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ász 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ász 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.
内核化、证明复杂性和社交选择.pdf