Description

In recent years a considerable progress in automated theorem proving and in
the formal representation of proofs has been achieved. Proof theory allows
for the automated analysis of such proofs as formal objects. In this
lecture, we provide the theoretical basis of this emerging field and give
an overview on recent developments and implementations. 

Plan of the lecture:
1.classical methods of cut-elimination
2.Herbrand analysis
3.functional interpretations and proof mining
4.cut-elimination by resolution (CERES)
5.CERES at work (including a system demonstration)