Norbert Preining:
Cut elimination and Orevkov's speed up result in strange surroundings

This talk will introduce projective geometry and a proof theoretic
approach to deal with it, especially a Gentzen style calculus for
projective geometry. One of the most important tools in
practical proving of theorems in projective geometry is the use
of sketches. We present a formalization of sketches and show the
equivalence between the full Gentzen system and sketches.
Finally we discuss using Orevkovs result on non-elementary speed
up between cut-free proofs and proofs using cut and how his ideas
and proof can be used to show that under certain circumstances
sketches are non-elementary slower than using cuts.