MINIMUM LENGTH EQUIVALENT FREGE PROOF

• INSTANCE: A Frege proof $\pi$ of a tautology $\varphi$.
• SOLUTION: A Frege proof $\pi'$ of $\varphi$ shorter than $\pi$, i.e., containing at most as many symbols as $\pi$.

• MEASURE: Number of symbols in $\pi'$.

  
  

• Good News: Approximable within O(n).

• Bad News: APX-hard [8].

• Comment: The result applies to all Frege systems, to all extended Frege systems, to resolution, to Horn clause resolution, to the sequent calculus, and to the cut-free sequent calculus. Not approximable within $2^{\log^{(1-\varepsilon )}n}$ for any $\varepsilon >0$ unless $NP\subseteq \mbox{\sc QP}$ [8].