Title :
Non-automatizability of bounded-depth Frege proofs
Author :
Bonet, Maria Luisa ; Domingo, Carlos ; Gavald, Ricard ; Maciel, Alexis ; Pitassi, Toniann
Author_Institution :
Dept. of Software, Univ. Politecnica de Catalunya, Barcelona, Spain
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
Keywords :
computational complexity; theorem proving; bounded-depth Frege proofs; deterministic polynomial-time algorithm; non-automatizability; Boolean functions; Circuits; Computer science; Interpolation; Large scale integration; Logic; Polynomials; Surface-mount technology;
Conference_Titel :
Computational Complexity, 1999. Proceedings. Fourteenth Annual IEEE Conference on
Conference_Location :
Atlanta, GA
Print_ISBN :
0-7695-0075-7
DOI :
10.1109/CCC.1999.766258