185.A45 Logic and Computability
This course is in all assigned curricula part of the STEOP.
This course is in at least 1 assigned curriculum part of the STEOP.

2020W, VU, 4.0h, 6.0EC, to be held in blocked form


  • Semester hours: 4.0
  • Credits: 6.0
  • Type: VU Lecture and Exercise
  • Format: Distance Learning

Learning outcomes

After successful completion of the course, students are able to distinguish and to apply important concepts, techniques, and results of formal logic and computability theory. Moreover, students who pass the fianl exams should be able to understand and to explain connections between topics like incompleteness of arithmetical calculi, undecidabiltiy, formal provability and expressibility.

Subject of course

  • advanced aspects of classical first order logic as specification tool
  • proof systems for classical first order logic, including  soundness and completeness proofs 
  • elements of model theory (Löwenheim-Skolem, compactness, expressibility)
  • principles of automated theorem proving
  • methods for handling identity  
  • comparison of types of inference systems 
  • elements of modal logic: Kripke semantics, temporal logics 
  • elements of intuitionistic logic and constructive proofs
  •  computational aspects of logic
  • undecidabilty of first order logic and its consequences
  • models of computation (Turing machines, lambda calculus)
  • elementary recursion theory
  • Church-Turing thesis
  • incompleteness of arithmetic and its consequences 

Teaching methods

  • derivations in various different logical calculi
  • applying formal concepts to standard problem sets
  • mastering formal (mathematical) definitions
  • analysis of proofs of central results

Mode of examination


Additional information

ETCS Breakdown:

6 ETCS = 150 hours

  • 38 hours:  lecture time (+ 8 hours repetitorium  for students not having a firm previous knowledge in logic)
  • 52 hours: 4 blocks of problems/exercises 
  • 60 hours: examination (preparation time)

The course will start Friday, October 9th, 11:00. The presentation class will be held live  in ZOOM:


Meeting ID: 979 7194 2086
Password: u=Q1$v7u 



Course dates

Fri11:00 - 13:0002.10.2020 - 11.12.2020 Logic and Computability
Tue14:00 - 16:0006.10.2020 - 26.01.2021 Logic and Computability
Thu11:00 - 13:0008.10.2020 - 10.12.2020 Logic and Computability
Fri11:00 - 13:0009.10.2020FAV Hörsaal 1 - INF Vorbesprechung
Fri14:00 - 16:0009.10.2020 - 06.11.2020FAV Hörsaal 1 - INF Tutorial
Fri14:00 - 16:0009.10.2020EI 7 Hörsaal - ETIT 185.A45 Logic and Computability 1st meeting
Logic and Computability - Single appointments
Fri02.10.202011:00 - 13:00 Logic and Computability
Tue06.10.202014:00 - 16:00 Logic and Computability
Thu08.10.202011:00 - 13:00 Logic and Computability
Fri09.10.202011:00 - 13:00 Logic and Computability
Fri09.10.202011:00 - 13:00FAV Hörsaal 1 - INF Vorbesprechung
Fri09.10.202014:00 - 16:00EI 7 Hörsaal - ETIT 185.A45 Logic and Computability 1st meeting
Fri09.10.202014:00 - 16:00FAV Hörsaal 1 - INF Tutorial
Tue13.10.202014:00 - 16:00 Logic and Computability
Thu15.10.202011:00 - 13:00 Logic and Computability
Fri16.10.202011:00 - 13:00 Logic and Computability
Fri16.10.202014:00 - 16:00FAV Hörsaal 1 - INF Tutorial
Tue20.10.202014:00 - 16:00 Logic and Computability
Thu22.10.202011:00 - 13:00 Logic and Computability
Fri23.10.202011:00 - 13:00 Logic and Computability
Fri23.10.202014:00 - 16:00FAV Hörsaal 1 - INF Tutorial
Tue27.10.202014:00 - 16:00 Logic and Computability
Thu29.10.202011:00 - 13:00 Logic and Computability
Fri30.10.202011:00 - 13:00 Logic and Computability
Fri30.10.202014:00 - 16:00FAV Hörsaal 1 - INF Tutorial
Tue03.11.202014:00 - 16:00 Logic and Computability
Course is held blocked

Examination modalities

  • solutions to 4 blocks of exercises - to be worked out self-reliantly
  • written exam
  • oral exam


DayTimeDateRoomMode of examinationApplication timeApplication modeExam
Thu11:00 - 13:0020.01.2022FAV Hörsaal 1 - INF written19.01.2022 00:00 - 19.01.2022 23:59TISSPrüfung WS2021

Course registration

Begin End Deregistration end
13.08.2020 12:00 06.12.2020 23:00 06.12.2020 23:00


Study CodeSemesterPrecon.Info
066 931 Logic and Computation 1. Semester


(see lecture slides for additional literature)

Previous knowledge

Knowledge of classical propositional logic and of basic concepts of classical first order logic (logical consequence, interpretations and model structures, satisfiability versus validity, acquaintance with various proof systems), a firm understanding of the syntax/semantic distinction, some experience with formal specification, acquaintance with a range of different programming paradigms (imperative, functional, logical),  and automata theory (finite automata, pushdown automata, Turing machines)

NB: If you don't have a firm background in logic yet, you are asked to join special repetitorium classes, which are open to all participants.

Preceding courses

Continuative courses