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.

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

Properties

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

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

Immanent

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 Monday, October 4th 2021, 11:00. The presentation class will be held live in ZOOM:


https://tuwien.zoom.us/j/91099333420?pwd=TFh5RWs4bnpqT3RoYk9DSzBZRGhJQT09

Meeting-ID: 910 9933 3420
Passwort: 6jHpGmJw

Lectures will be pre-recorded and accessible via TUWEL. In addition we plan to offer a physical meeting every Thursday 11:15-13:00, starting with October 7th, 2021. Tutorial sessions for the Logic part will take place on Monday, October 11, 18, 25 and November 8, 11:00-13:00. 

Note that you can attend the in person classes, only if you comply with the 3-G access rules.

 

Lecturers

Institute

Course dates

DayTimeDateLocationDescription
Mon11:00 - 13:0004.10.2021 - 13.12.2021FAV Hörsaal 1 Helmut Veith - INF Lecture
Thu09:00 - 11:0007.10.2021 - 16.12.2021FAV Hörsaal 1 Helmut Veith - INF Exercise
Thu11:00 - 13:0007.10.2021 - 16.12.2021FAV Hörsaal 1 Helmut Veith - INF Lecture
Logic and Computability - Single appointments
DayDateTimeLocationDescription
Mon04.10.202111:00 - 13:00FAV Hörsaal 1 Helmut Veith - INF Lecture
Thu07.10.202109:00 - 11:00FAV Hörsaal 1 Helmut Veith - INF Exercise
Thu07.10.202111:00 - 13:00FAV Hörsaal 1 Helmut Veith - INF Lecture
Mon11.10.202111:00 - 13:00FAV Hörsaal 1 Helmut Veith - INF Lecture
Thu14.10.202109:00 - 11:00FAV Hörsaal 1 Helmut Veith - INF Exercise
Thu14.10.202111:00 - 13:00FAV Hörsaal 1 Helmut Veith - INF Lecture
Mon18.10.202111:00 - 13:00FAV Hörsaal 1 Helmut Veith - INF Lecture
Thu21.10.202109:00 - 11:00FAV Hörsaal 1 Helmut Veith - INF Exercise
Thu21.10.202111:00 - 13:00FAV Hörsaal 1 Helmut Veith - INF Lecture
Mon25.10.202111:00 - 13:00FAV Hörsaal 1 Helmut Veith - INF Lecture
Thu28.10.202109:00 - 11:00FAV Hörsaal 1 Helmut Veith - INF Exercise
Thu28.10.202111:00 - 13:00FAV Hörsaal 1 Helmut Veith - INF Lecture
Thu04.11.202109:00 - 11:00FAV Hörsaal 1 Helmut Veith - INF Exercise
Thu04.11.202111:00 - 13:00FAV Hörsaal 1 Helmut Veith - INF Lecture
Mon08.11.202111:00 - 13:00FAV Hörsaal 1 Helmut Veith - INF Lecture
Thu11.11.202109:00 - 11:00FAV Hörsaal 1 Helmut Veith - INF Exercise
Thu11.11.202111:00 - 13:00FAV Hörsaal 1 Helmut Veith - INF Lecture
Mon15.11.202111:00 - 13:00FAV Hörsaal 1 Helmut Veith - INF Lecture
Thu18.11.202109:00 - 11:00FAV Hörsaal 1 Helmut Veith - INF Exercise
Thu18.11.202111:00 - 13:00FAV Hörsaal 1 Helmut Veith - INF Lecture
Course is held blocked

Examination modalities

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

Exams

DayTimeDateRoomMode of examinationApplication timeApplication modeExam
Tue13:00 - 15:0028.05.2024EI 5 Hochenegg HS written03.04.2024 10:00 - 27.05.2024 23:59TISSL&C 3rd written exam

Course registration

Begin End Deregistration end
12.08.2021 12:00 05.12.2021 23:00 05.12.2021 23:00

Curricula

Study CodeObligationSemesterPrecon.Info
066 931 Logic and Computation Mandatory1. Semester

Literature

(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

Language

English