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.[ref]
The Relative Efficiency of Propositional Proof Systems by Stephen Cook and Robert A. Reckhow. §1, Definition 1.3 and discussion on pp.38–39
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.[ref]
New to topics? Read the docs here!