Oberseminar "Mathematische Logik" - Prof. Dr. Christian Glaßer

Cook and Reckhow defined the term "proof system" in 1979. A typical example is the resolution calculus, which can be used to prove that a propositional formula is a tautology. For some tautologies, the shortest resolution proofs have exponential length. If we can recognize some of these tautologies with shorter "special arguments", then we can extend the resolution calculus by these special arguments and obtain a better proof system (better, because some tautologies now have shorter proofs).
This leads to the still open question of whether there is a best (so-called optimal) proof system for tautologies. Actually the question is not restricted to tautologies, it is also interesting for arbitrary enumerable sets. Here we know the following: All sets in NP trivially have optimal proof systems. However, so far no enumerable sets outside NP have been found that have optimal proof systems.
The talk summarizes the research of our group and shows how the difficulty of these questions can be explained by oracle constructions.