short proof

F_d versus F_{d+1} โ˜…โ˜…โ˜…

Author(s): Krajicek

Problem   Find a constant $ k $ such that for any $ d $ there is a sequence of tautologies of depth $ k $ that have polynomial (or quasi-polynomial) size proofs in depth $ d+1 $ Frege system $ F_{d+1} $ but requires exponential size $ F_d $ proofs.

Keywords: Frege system; short proof

Syndicate content