Prof. Tobias Nipkow, Sommersemester 2018
- TUMonline: IN2049 SS18
- 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: 9.4. First exercise: 10.4.
- Tutors: Lars Hupel
- 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:00-14:00, MI 01.11.018. The change is reflected in TUMonline.
- 23.04.: An error on sheet 2 has been fixed.
- 05.04.: First exercise sheet is available.
- Website created
Homework BonusThere 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.
SubmissionTypically before the tutorial in the week after (see sheet). Submission at the start of the tutorial or to the tutor's email address.
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.
- 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)
- 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.