Corelab Seminar

Thodoris Papamakarios
Proof Complexity: A Tableaux Perspective

The method of semantic tableaux is arguably one of the most elegant proof systems. Unfortunately, it hasn't received much attention in the proof complexity literature, mainly due to some early negative results, e.g., that sometimes cut-free tableaux perform worse than truth-tables. We wish to bring tableaux back to the picture, showing in an elegant-uniform way several known results spanning proof complexity, from a tableaux viewpoint.