= Robert A. Reckhow
{c}
<Robert A. Reckhow> coauthored the 1979 paper establishing a general computational framework for <propositional proof systems> with <Stephen Cook>. Their formulation represents a proof system by a polynomial-time computable surjection onto the <logical tautologies>, separating verification cost from the length of the shortest proof.<The Relative Efficiency of Propositional Proof Systems by Stephen Cook and Robert A. Reckhow>[§1, Definition 1.3 and discussion on pp.38–39]{ref}
The paper compares systems using efficient translations of proofs. If proofs in one system can be converted to proofs in another by a polynomial-time procedure, the translated proofs can grow only polynomially in length. Such a comparison is stronger than observing that both systems eventually prove the same formulas: completeness alone places no useful bound on the cost of converting evidence. This gives <proof complexity> a way to compare proof formats as computational representations.<The Relative Efficiency of Propositional Proof Systems by Stephen Cook and Robert A. Reckhow>[§1, Definition 1.5, p-simulation]{ref}
Back to article page
