Prof. Tobias Nipkow, Sommersemester 2016


  • View your graded final exams on Friday, August 19, 2016:
    • The exams are graded and preliminary grades should be viewable in TUMOnline.
    • You can view the exams on Friday, August 19 in Simon Wimmer's office.
    • Last names beginning with A-L please use the time slot from 10:00 to 11:00, and last names beginning with M-Z please use the time slot from 11:00 to 12:00.
  • Exam on July 26:
    • You are allowed to bring two hand-written cheat sheets; size DIN A4, the frontsides and backsides may be filled.
    • You will need to write down the rules for proof calculi yourself (i.e. they will not be handed out with the exam). However, you do not need rules for the Hilbert calculus.
  • No tutorial on April 27 due to Fachschaftsvollversammlung (FVV). Submit your homework before the usual time to our offices or via email.


Homework Bonus

There will be graded homework assignments. Who achieves more than 50% of the homework score, gets a bonus of 0.3/0.4 on the final exam's grade, provided the exam is passed.


Typically before the tutorial in the week after (see sheet). Submission at the start of the tutorial, to the tutors' offices or to the tutors' emails.



The course assumes that you have had a basic introduction to logic already and are familiar with the following topics: syntax and semantics of both propositional and first-order logic; disjunctive and conjunctive normal forms; basic equivalences of propositional and first-order logic. These topics will only be refreshed briefly at the beginning of the course. The first half of the course will introduce the basic theory of first-order logic: normal forms of first-order formulas, compactness, undecidability, Herbrand theory, resolution. The second half of the course focuses on two important proof systems (sequent calculus and natural deduction), on the incompleteness of arithmetic and on decision procedures for fragments of logic and arithmetic.

Topics and Slides

Propositional logic: First-order predicate logic:


The first half of the course is based on this booklet:
  • Uwe Schöning. Logik für Informatiker (English: Logic for Computer Scientists).
The topics in the second half are not covered by any one book. The following references cover some of them, but may use their own notation:
  • Ebbinghaus, Flum, Thomas. Einführung in die mathematische Logik (English: Mathematical Logic).
  • Herbert Enderton. A Mathematical Introduction to Logic.
  • Melvin Fitting. First-Order Logic and Automated Theorem Proving.
  • Jean Gallier. Logic for Computer Science.
  • John Harrison. Handbook of Practical Logic and Automated Reasoning.
  • A. Troelstra and H. Schwichtenberg. Basic Proof Theory.