Title :
Hard examples for bounded depth Frege
Author_Institution :
Inst. of Comput. Sci., Hebrew Univ., Jerusalem
fDate :
6/24/1905 12:00:00 AM
Abstract :
We prove exponential lower bounds on the size of a bounded depth Frege proof of a Tseitin graph-based contradiction, whenever the underlying graph is an expander. This is the first example of a contradiction, naturally formalized as a 3-CNF, that has no short bounded depth Frege proofs
Keywords :
computational complexity; theorem proving; Tseitin graph-based contradiction; bounded depth Frege proof; expander; exponential lower bounds; hard examples; Approximation algorithms; Computational complexity; Turning; Writing;
Conference_Titel :
Computational Complexity, 2002. Proceedings. 17th IEEE Annual Conference on
Conference_Location :
Montreal, Que.
Print_ISBN :
0-7695-1468-5
DOI :
10.1109/CCC.2002.1004323
