Logic
Prof. Tobias Nipkow, Sommersemester 2018
 TUMonline: IN2049 SS18
 Lectures: Monday, 08:30–10:00 in HS3 00.06.011, and Wednesday, 08:3010:00 in HS3 00.06.011

Exercises: Tuesday, 10:15–11:45 in MI 00.08.038
 Start: 9.4. First exercise: 10.4.; last: 3.7.
 Tutors: Lars Hupel
 Exams: 23.7., 13:30, MW 1050 (surnames A through L), MW 2050 (surnames M through Z)
News
 09.07.: The last tutorial (on 10.07.) is cancelled. Instead, there will be office hours at the same time (10:15–11:45) in MI 00.09.039. Bring any questions related to the lecture, tutorial, or homework.
 29.06.: Updated Homework 12.3: a restriction was missing; F must not contain any quantifiers.
 22.06.: Updated Exercise 11.4: one branch of the ND tree applied conjunction and existential elimination in the wrong order.
 11.06.: Updated Homework 9.3: there was another, more severe error in the assignment. A fixed version has been uploaded, but we have decided to award 0 points because the problem was impossible to solve.
 06.06.: Updated Homework 9.3: the formulas representing instructions were wrong; this has been updated.
 15.05.: Updated Homework 6.2: there was a closing parenthesis missing.
 15.05.: Updated exercise sheet 6 again to reflect the changed deadline for homework.
 15.05.: The tutorial on 22.05. is cancelled because of Whitsun Vacation (Pfingstferien). The replacement tutorial is on Wednesday, 23.05., 12:00–14:00, MI 00.13.054. The change is reflected in TUMonline.
 14.05.: Updated Exercise 6.3 and Homework 6.2. Please download an updated version of sheet 6.
 27.04.: The tutorial on 08.05. is cancelled because of the student assembly. The replacement tutorial is four hours later: 14:00–16:00, MI 00.13.054. The change is reflected in TUMonline.
 24.04.: Homework for sheet 3 is due via email or on paper in Lars' office (MI 00.09.063) by Wednesday, 02.05.2018, 12:00.
 24.04.: The tutorial on 01.05. is cancelled because of public holiday. The next tutorial will be on Monday, 30.04., 12:0014:00, MI 01.11.018. The change is reflected in TUMonline.
 23.04.: An error on sheet 2 has been fixed.
Excercises
Homework Bonus
There will be graded homework assignments. Anyone who achieves more than 50% of the homework score gets awarded a bonus of 0.3 on the final exam's grade, provided the exam is passed.Submission
Typically before the tutorial in the week after (see sheet). Submission at the start of the tutorial or to the tutor's email address.Material
 Sheet 1 (Solution)
 Sheet 2 (Solution)
 Sheet 3 (Solution)
 Sheet 4 (Solution)
 Sheet 5 (Solution)
 Sheet 6 (Solution)
 Sheet 7 (Solution)
 Sheet 8 (Solution)
 Sheet 9 (Solution)
 Sheet 10 (Solution)
 Sheet 11 (Solution)
 Sheet 12 (Solution)
 Sheet 13 (Solution)
Contents
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 firstorder logic; disjunctive and conjunctive normal forms; basic equivalences of propositional and firstorder logic. These topics will only be refreshed briefly at the beginning of the course.
The main topics of the course:
 Proof theory: sequent calculus, natural deduction, resolution; their soundness and completeness; translations between proof systems.
 Metatheory of first order logic: compactness, model theoy, undecidability, incompleteness of arithmetic.
 Decision procedures for fragments of logic and arithmetic.
Slides
Propositional logic:
 Basics (Esparza/Schöning)
 Equivalences (Esparza/Schöning)
 Normal forms (Esparza/Schöning)
 Definitional CNF (Harrison)
 Horn formulas (Esparza/Schöning)
 Compactness (Harrison)
 Resolution (Esparza/Schöning)
 Basic proof theory (Troelstra&Schwichtenberg)
 Basics (Esparza/Schöning)
 Normal forms (Esparza/Schöning)
 Herbrand theory (Esparza/Schöning)
 Resolution (Esparza/Schöning)
 Equality (Esparza)
 Undecidability (Cutland)
 Compactness (Harrison)
 The Classical Decision Problem (Harrison)
 Basic proof theory (Troelstra&Schwichtenberg)
 Theories (Harrison)
 Quantifier Elimination (Harrison/Enderton)
Literature
 Ebbinghaus, Flum, Thomas. Einführung in die mathematische Logik (English: Mathematical Logic).
 Herbert Enderton. A Mathematical Introduction to Logic.
 Melvin Fitting. FirstOrder Logic and Automated Theorem Proving.
 Jean Gallier. Logic for Computer Science.
 John Harrison. Handbook of Practical Logic and Automated Reasoning.
 Uwe Schöning. Logik für Informatiker (English: Logic for Computer Scientists).
 A. Troelstra and H. Schwichtenberg. Basic Proof Theory.