Fall 2018

On small-depth Frege proofs for Tseitin for grids

Wednesday, Nov. 7, 2018 10:30 am12:00 pm PST

Add to Calendar


Johan Håstad (KTH Royal Institute of Technology)


Room 116

We prove that a small-depth Frege refutation of the Tseitin contradiction on the grid requires subexponential size. We conclude that polynomial size Frege refutations of the Tseitin contradiction must use formulas of almost logarithmic depth.