Extracting exact time bounds from logical proofs