Fall 2018

On small-depth Frege proofs for Tseitin for grids

Wednesday, November 7th, 2018, 10:30 am12:00 pm

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.