P. Pudlak's lectures at the
This will be a continuation of my last year School, or of my talk at the EMS Weekend. I will show that the principle $B_4$ is tractable (provable in $S^1_2$ and decidable in polynomial time). It is a result of Hastad (obtained at the last year School). The aim of this research is to find principles that would play a role in proof complexity similar to the role of Sipser functions in computational complexity.
Fall school(Sept.'04)
Hard principles based on games