4 ms·
Hmmm, isn't the number of proofs to check normally exponential in the length of the proof? E.g. if there are n proofs with length k (characters, applications o
by schoen 3y ago
Hmmm, isn't the number of proofs to check normally exponential in the length of the proof?
E.g. if there are n proofs with length k (characters, applications of rules of inference, intermediate steps), shouldn't there be n² proofs with length 2k? (In some systems you can prune some, but the extent to which you can do that would depend on the representation of the proof and the allowable inferences.)
- eru 3y agoDetails depend on the proof system. But yes, in general you expect that the number of possible proofs goes up exponentially with their length. But any single given proof can be checked in polynomial time. That's almost the definition of NP: NP stands for 'nondeterministic polynomial time'. Which means if you can nondeterministically 'guess' a solution (or someone hands it to you etc), you can verify it in polynomial time.
- schoen 3y agoOh right, that makes perfect sense. Thanks.