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

### MINIMUM LENGTH EQUIVALENT FREGE PROOF

- INSTANCE: A Frege proof of a tautology .
- SOLUTION: A Frege proof of shorter than , i.e., containing at most as many symbols as .

- MEASURE: Number of symbols in .

- 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 for any unless [8].