Abstract.
In this paper, we show how to extend the argument due to Bonet, Pitassi and Raz to show that bounded-depth Frege proofs do not have feasible interpolation, assuming that factoring of Blum integers or computing the Diffie–Hellman function is sufficiently hard. It follows as a corollary that bounded-depth Frege is not automatizable; in other words, there is no deterministic polynomial-time algorithm that will output a short proof if one exists. A notable feature of our argument is its simplicity.
Similar content being viewed by others
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Bonet, M.L., Domingo, C., Gavaldà, R. et al. Non-Automatizability of Bounded-Depth Frege Proofs. comput. complex. 13, 47–68 (2004). https://doi.org/10.1007/s00037-004-0183-5
Received:
Issue Date:
DOI: https://doi.org/10.1007/s00037-004-0183-5