Logic

Overview

Questions regarding the lecture and exercises can be discussed on Zulip. You can subscribe to all Logic-* streams by visiting this stream and clicking the Alice emoji.

Organization

The lectures will be live on BBB and will be recorded. Please join with your audio and video off. If you have a question during the lecture, you can either ask it via audio or post it in the public chat. In case the lecturer overlooks a question in the chat (this can happen easily) you may need to use your audio.

The recordings are also on BBB. Publication of the recordings takes about a day and is not under our control.

Prerequesites

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.

Content

Logic is the science of reasoning. It plays an important role in many disciplines, including mathematics (where it originated) and philosophy, but it is particularly central to computer science and sometimes referred to as the calculus of computer science. We emphasise the computational aspects of logic. These are the central topics of the course:

1. We learn how to perform proofs in multiple deductive systems, how to prove the soundness and completeness of a system with respect to a semantics, and how to translate proofs between systems. In particular we cover resolution, natural deduction, sequent calculus and Hilbert systems.
2. We learn about the limitations of first-logic and the relationship between logic and computability.
3. We learn how to solve logical problems algorithmically using (semi-)decision procedures like resolution (for pure logic) and quantifier elimination (for arithmetic).

Lecture Material

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)
• Sequent Calculus (Troelstra&Schwichtenberg)
• Tableaux Calculus
• Natural Deduction (Troelstra&Schwichtenberg)
• Hilbert Systems (Troelstra&Schwichtenberg)

First-order logic:

• 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

1. Uwe Schöning. Logik für Informatiker (English: Logic for Computer Scientists).
2. A. Troelstra and H. Schwichtenberg. Basic Proof Theory.
3. Jean Gallier. Logic for Computer Science.
4. John Harrison. Handbook of Practical Logic and Automated Reasoning.
5. Melvin Fitting. First-Order Logic and Automated Theorem Proving.
6. Herbert Enderton. A Mathematical Introduction to Logic.
7. Ebbinghaus, Flum, Thomas. Einführung in die mathematische Logik (English: Mathematical Logic).