MINIMUM LENGTH EQUIVALENT FREGE PROOF

Next: Miscellaneous Up: Propositional Logic Previous: MAXIMUM K-CONSTRAINT SATISFACTION Index

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].

Viggo Kann
2000-03-20