Non-Automatizability of Bounded-Depth Frege Proofs

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 DiffieHellman 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.

• Type: Conference
• Year: 1999
• Where: COCO
• Authors: Maria Luisa Bonet, Carlos Domingo, Ricard Gavaldà, Alexis Maciel, Toniann Pitassi
• Keywords: Algorithms, Bounded-depth Frege, Bounded-depth Frege Proofs, COCO 1999, Deterministic Polynomial-time Algorithm