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
- Start: 24.04. First exercise: TBD
- Tutors: Lars Hupel
- Website created
SubmissionTypically before the tutorial in the week after (see sheet). Submission at the start of the tutorial, to the tutor's office 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.
- 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.