I read no superpolynomial lower bound is known for the length (number of symbols) of zeroth order logic Frege proofs. My question is: what is the best upper bound known? I.e. given a tautology $f$ of length $n$, what length is sufficient to prove $f$?


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.