• DocumentCode
    1632314
  • Title

    Hard examples for bounded depth Frege

  • Author

    Ben-Sasson, Eli

  • Author_Institution
    Inst. of Comput. Sci., Hebrew Univ., Jerusalem
  • fYear
    2002
  • fDate
    6/24/1905 12:00:00 AM
  • Firstpage
    4
  • Lastpage
    4
  • 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;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Computational Complexity, 2002. Proceedings. 17th IEEE Annual Conference on
  • Conference_Location
    Montreal, Que.
  • ISSN
    1093-0159
  • Print_ISBN
    0-7695-1468-5
  • Type

    conf

  • DOI
    10.1109/CCC.2002.1004323
  • Filename
    1004323
    • Link To Document
    https://search.isc.ac/dl/search/defaultta.aspx?DTC=49&DC=1632314