According to Krajícek, Jan and Pavel Pudlák. “Some Consequences of Cryptographical Conjectures for S12 and EF.” Inf. Comput. 140 (1998): 82-94., the extended Frege proof system is not automatizable unless RSA is not secure. Now I have an argument about the unautomatizability of extended resolution: Suppose RSA is secure. Assume that extended resolution is automatizable, then there exists a machine $M$ that takes an unsatisfiable CNF formula $\varphi$, then outputs an ER-proof of the unsatisfiability of $\varphi$ in time bounded by a polynomial of the size of the shortest ER proof of $\varphi$. Now construct a machine $M'$ that does the follows: For a given unsatisfiable CNF formula $\varphi$, call $M$ to obtain one of its ER proofs $M(\varphi)$, then translate the proof into an EF proof (this can be done very easily). Since the size of the shortest EF proof is linear with the size of the shortest ER proof, the time $M$ needed is bounded by a polynomial of the size of the shortest EF proof of $\varphi$. Therefore, $M'$ produces an EF proof of $\varphi$ in polynomial time, which contradicts the fact that EF is not automatizable. Hence the assumption is incorrect, and ER is not automatizable.

Is my argument correct?

  • 3
    $\begingroup$ Yes, automatizability is clearly preserved by passing to a p-equivalent proof system. $\endgroup$ Jun 7, 2023 at 13:29


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.