To learn about techniques of automated proof transformations and semi-automated analysis of mathematical proofs.
The system CERES for automated cut-elimination by resolution. Extension of CERES by development of higher input- and output-languages, experiments with cut-elimination in mathematical proofs. Participants have to attend the weekly meetings of the CERES project group
details of the course can be found on www.logic.at/lvas/185302
For successfully completing the course the following is needed: (1) development of a program, (2) writing a report (about ten pages), (3) presentation of the work in a CERES project meeting.
Not necessary