Logic
Prof. Tobias Nipkow, Sommersemester 2017
- TUMonline: Logic (IN2049)
- Lectures: Monday, 08:30–10:00 in HS3 00.06.011, and Wednesday, 08:30-10:00 in HS3 00.06.011
-
Exercises: Tuesday, 10:15–11:45 in MI 00.08.038
- Start: 24.04. First exercise: 26.04.
- Tutors: Lars Hupel
- Exams: Friday, 04.08.2017, and Thursday, 05.10.2017 (repeat exam).
News
- 19.09.: The repeat exam will take place as a written exam on 05.10.2017.
- 17.08.: In case only a small number of students register for the repeat exam, the written exam will be substituted by an oral exam. Dates for the oral exam: 25.09.–28.09.
- 28.07.: Exam review will be on Monday, 21.08., 14:00-16:00, in room MI 00.09.038.
- 24.07.: You are allowed to bring two hand-written cheat sheets (size DIN A4) to the exam. No other material is allowed, in particular printed sheets.
- 24.07.: There will be office hours (Sprechstunde) on Friday, 28.07., 14:00-16:00, in room MI 00.09.038. You can ask any question related to the lecture, exercises or homework.
- 27.06.: Two mistakes in the solution for sheets 7 (Exercise 7.1) and 8 (Exercise 8.3) have been fixed.
- 21.05.: Next tutorial on Tuesday, 23.05.2017, had to be moved to 14:00 because of SVV. Apologies for this inconvenience. Check your email inbox for information about the room.
- 15.05.: Next tutorial is Tuesday, 16.05.2017.
- 11.05.: Clarified bonus.
- 08.05.: The next tutorial is Wednesday, 10.05.2017, starting 14:30.
- 18.04.: Note the changed tutorial details. Due to the high number of class enrollments, we will reschedule the first four tutorials to Wednesday, 14:30–16:00, in Intermishörsaal 1. First tutorial: Wednesday, 26.04.
- Website created
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
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 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 main topics of the course:
- Proof theory: sequent calculus, natural deduction, resolution; their soundness and completeness; translations between proof systems.
- Meta-theory 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. First-Order 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.