Evaluation
- There are weekly exercises that count 50 % of the overall grade and a project that counts another 50 %.
- Solved exercises must be marked and uploaded in OLAT. The deadline is Thursday, 6 am before the lecture. Solutions will be made available in OLAT.
- The projects are available as PDF and as Isabelle theories.
- The projects will be presented on April 25, and then also the project distribution will be conducted. Each project is designed for 1, 2 or 3 persons.
- The deadline for handing in completed projects is August 1.
- Evaluation of projects is based on
- number and significance of remaining sorrys
- readability and clarity of submitted Isabelle theory
- successful document generation of submitted Isabelle theory
- personal interview on each project, where project related questions will be asked
- Project assignment
- Congruence Closure: IS + FH + SG
- Propositional Logic: EP + HP