DocumentCode :
2822143
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
fYear :
1999
fDate :
1999
Firstpage :
15
Lastpage :
23
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;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Computational Complexity, 1999. Proceedings. Fourteenth Annual IEEE Conference on
Conference_Location :
Atlanta, GA
ISSN :
1093-0159
Print_ISBN :
0-7695-0075-7
Type :
conf
DOI :
10.1109/CCC.1999.766258
Filename :
766258
Link To Document :
بازگشت