Logic
Prof. Tobias Nipkow, Sommersemester 2016
 TUM Online: Logic (IN2049)
 Lectures: Tuesday, 12:15  13:45 in HS3 00.06.011, and Wednesday, 8:30  10:00 in HS2 00.04.011

Exercises: Wednesday, 10:15  11:45 in
Konrad Zuse (MI 01.11.018)
Due to the high number of class enrollments, we will reschedule the first four tutorials to Wednesday, 12:15  13:45 in MI 00.13.009A
The tutorial is scheduled to the original room and time slot beginning with April 20  Start: 12.4. First exercise: 13.4
 Tutors: Peter Lammich, Simon Wimmer
News
 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 AL please use the time slot from 10:00 to 11:00, and last names beginning with MZ please use the time slot from 11:00 to 12:00.
 Exam on July 26:
 You are allowed to bring two handwritten 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.
Excercises
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.Submission
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.Material
 Exercise Sheet 1 [ Tutorial Notes ] [ Homework Solution ]
 Exercise Sheet 2 [ Homework Solution ]
 Exercise Sheet 3 [ Homework Solution ]
 Exercise Sheet 4 [ Homework Solution ]
 Exercise Sheet 5 [ Homework Solution ]
 Exercise Sheet 6 [ Homework Solution ]
 Exercise Sheet 7 [ Homework Solution ]
 Exercise Sheet 8 [ Homework Solution ]
 Exercise Sheet 9 , Original paper on Cooper's algorithm [ Homework Solution ]
 Exercise Sheet 10 (Corrected hw 10.1) [ Homework Solution ] [ Sequent solver in Isabelle with document ]
 Exercise Sheet 11 (Corrected hw 11.2) [ Homework Solution ]
 Exercise Sheet 12 [ Homework Solution ]
 Exercise Sheet 13 [ Homework Solution ]
 Exercise Sheet 14
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 first half of the course will introduce the basic theory of firstorder
logic: normal forms of firstorder 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:
 Basics (Esparza/Schöning)
 Equivalences (Esparza/Schöning)
 Normal forms (Esparza/Schöning)
 Definitional CNF (Esparza/Schöning)
 Horn formulas (Esparza/Schöning)
 Compactness (Esparza/Schöning)
 Resolution (Esparza/Schöning)
 Basics (Esparza/Schöning)
 Normal forms (Esparza/Schöning)
 Undecidability (Cutland)
 Herbrand theory (Esparza/Schöning)
 Resolution (Esparza/Schöning)
 Equality (Esparza)
 The Classical Decision Problem (Harrison)
 Theories (Harrison)
 Quantifier Elimination (Harrison/Enderton)
 Undecidability and incompleteness of arithmetic (Ebbinghaus, Flum, Thomas; Chapter X)
 Basic proof theory
Literature
The first half of the course is based on this booklet: Uwe Schöning. Logik für Informatiker (English: Logic for Computer Scientists).
 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.
 A. Troelstra and H. Schwichtenberg. Basic Proof Theory.