Logic 1, Spring 2026
On this page, you may find the specifics to the Logic 1 course. You may find on the general Logic courses page detailed information on lecture notes, communication and grading, which apply to both this and the Logic 2 course. In particular make sure to study the Logic Rondo lecture notes before the lectures.
The course will be organised as follows. Throughout the semester, there are 7 lectures and exercise classes, see the Course Schedule for details. You will have to submit homework assignments and the grade of the homework will make 30% of your final grade and the course will end with an exam, which makes 70% of your final grade, see the Exam times section below. You will have to have a passing grade for both the exam and the final grade. Details can be found on the common Logic page.
Course Schedule
The lectures take place weekly in Gorleaus C4/5 (Saucer) except for the second lecture according to the timetable below, while the exercise classes take are in various rooms, see Practical Rooms below. The homework deadlines will be available on Brightspace.
Here is the timetable of the course, numbered by semester week:
| Week | Lecture | Practical |
|---|---|---|
| 1 | Lecture 1 (Mon, 02 Feb, 13:15) | Thu, 05 Feb, 13:15 |
| 2 | Lecture 2 (Mon, 09 Feb, 09:00, in C3) | Thu, 12 Feb, 13:15 |
| 3 | Lecture 3 (Mon, 16 Feb, 13:15) | Thu, 19 Feb, 13:15 |
| 4 | Lecture 4 (Mon, 23 Feb, 13:15) | Thu, 26 Feb, 13:15 |
| 5 | Lecture 5 (Mon, 02 Mar, 13:15) | Thu, 05 Mar, 13:15 |
| 6 | Lecture 6 (Mon, 09 Mar, 13:15) | Thu, 12 Mar, 13:15 |
| 7 | Lecture 7 (Mon, 16 Mar, 13:15) | Thu, 19 Mar, 13:15 |
| 8 | Exam on Fri, 27 Mar, 08:00 | – |
After this, Logic 2 continues on Mondays.
You may find the content of the lectures below.
Lecture 1
Introduction and history, syntax of propositional logic (PL), translating natural language to formulas, parse trees, subformulas
Lecture 2
Deductive systems, natural deduction (ND) in sequent style, derivations (proof trees), machine-checked proofs
Lecture 3
Fitch-style natural deduction, truth tables, satisfiability, tautologies, classical ND (cND) for PL (proof by contradiction)
Lecture 4
Intro first-order logic (FOL): motivation, language, variables and binding
Lecture 5
Proof Theory of FOL, Substitution, natural deduction for intuitionistic FOL (ND₁) and classical FOL (cND₁), Fitch-Style proofs in ND₁
Lecture 6
Machine-checked proofs and proof-assistants for FOL, unification
Lecture 7
Proof normalisation, Herbrand’s theorem, First-Order Horn Clauses for Automatic Deduction
Practical Rooms
You will be distributed over rooms through enrolling in exercise groups on Brightspace at the beginning of the course. The following table shows the detailed list of rooms where exercise classes take place and which exercise group is assigned to each.
| Room | Groups |
|---|---|
| Gorlaeus Building - BM.1.23 | 1-8 |
| Gorlaeus Building - BM.1.26 | 9-13 |
| Gorlaeus Building - BM.1.33 | 14-20 |
| Gorlaeus Building - BW.0.18 | 21-23 |
| Gorlaeus Building - BW.0.06 (*) | 24-27 |
(*) The rooms in the BW wing are currently being worked on. The groups 24-27 will have the following changes:
- 05 Feb: BW.0.17
- 12 Feb: BW.0.06
- 19 Feb: DM.1.09
- From 26 Feb always in BW.0.06
Exam Times
The exam and retake take place in the University Sports Centre are scheduled for
- Fri, 27 Mar, 08:00 and
- Tue, 23 Jun, 13:00, respectively.