transformation to normal form, semantic trees, unification, resolution, resolution refinements, paramodulation, experiments with theorem provers. Didactic procedure: during the course two groups of exercises will be distributed; the exercises have to be solved by using the theorem prover prover9. Final oral examination.
ECTS breakdown
54h: 18 lectures a 2h + 1h preparation
8h: solving first sheet of ex. a 7 ex.
2h: typing solution in LaTeX
8h: downloading and testing prover9
34h: solving second sheet of exercises a 7 ex. (by use of prover9)
3h: typing solutions in LateX
40h: preparaton for final examination
1h: final examination
---------------------------------------------------------------------
150 h = 6 ECTS
