en | de

Automated Theorem Proving

master program

VO2 + PS1  WS 2013/2014  703608 + 703609


room consultation hours
VO + PS Georg Moser 1N05 Wednesday12:00 – 14:00

Time and Place

VO Wednesday 15:15 - 17:00 3W03 Georg Moser
PS Wednesday 17:15 - 18:00 3W03 Georg Moser

The lecture starts on October 2

Please register online for the lecture (till October 31, 23:59 Uhr) and the excercise group (till September 30, 23:59 Uhr).

Second Exam on July 11, 2014

The second exam will take place on July 11 at 12 pm in 3W04. Please register online for the exam.

First Exam on February 28, 2014

The first exam took place on February 28 @ 16:00 in 3W03.

exam    solution (corrected 09.04.14)

Please come by in the office hours of the lecturer, if you have any question regarding your exam papers.


The module "Automated Reasoning" comes with a proseminar. In this proseminar (programming) exercises for the lectures of the module will be posed. In particular it is expected that the students come up with their own implementation of a first-order resolution prover. Existing implementation are available online.

Grading Scheme

The following case distinction is employed to deduce your final mark.
   Points    Mark       Points    Mark       Points    Mark
>= 90 Very Good       >= 60 Acceptable       < 50 Failed
>= 75 Good >= 50 Pass