Information on the course

Applied Logic (2ITX0)

This is the information about the 5 ects elective course Applied Logic 2ITX0, starting in November 2021.

Due to the Covid19 restrictions the lectures are not allowed to be held on campus. Instead they will be given (in slightly shorter version) online in Canvas BigBlueButton or MSTeams. These will be recorded. We are happy to announce that all tutorials and the practical support will be offered on campus. As an extra service also the lectures recorded in 2019/2020 are available on
Video lectures.


The lecturers are


Goals:
In this course, you learn

Required background for this course is Logic and Set Theory, and some programming skills.

Course format:
The format of the course consists of the following ingredients:
number lecturer Nov 24 Dec 1 Dec 8 Dec 15 Dec 22 Jan 12 Jan 19
1 Rick Erkens Atlas 4.225 - Atlas -1.825 Atlas -1.825 online online Atlas -1.825
2 Joris Geurts Atlas 6.225 Atlas 4.225 Atlas 2.225 Atlas -1.310 online online online
3 Lars van den Haak AUD 13 AUD 13 Atlas 6.208 Atlas 10.330 online online Atlas 4.225
4 Nathan Cassee AUD 14 AUD 14 AUD 14 AUD 14 online online AUD 14
5 Jeroen Keiren Fenix 0.138 Helix West 4.91 Helix West 4.91 joined with group 6 joined with group 6 joined with group 6 joined with group 6
6 Roel Bloo Helix West 4.91 Matrix1.116 Matrix1.116 Matrix1.116 online online Matrix1.116

Registration for these groups can be done via Canvas.
  • Practical support, on Friday 8:45-10:30, on November 19 and 26, and December 10. Here you get support for using the computer tools by student assistants. The location was AUD 14 and AUD 15. These rooms are next to each other, just choose a room with free space. Also an online variant of this service will be offered via the following link.
  • Interim tests on Friday 9:00-10:00, on December 3 and 17, and January 14
    Assessment:
    The course is concluded by a written examination that counts for 50 %. It is a 'closed book' examination: on this examination using books and/or notes is not allowed. The grade for this examination should be at least 5 in order to pass for the course.

    The material for the examination consists of the sets of slides provided below

    Apart from that there are three assignments that should be done by every student individually, and count for 10 % each. uploaded in the ANS system (via https://secure.ans-delft.nl/) on December 3 and 17 and January 14, before 23:59.

    Finally, on the same dates December 3 and 17 and January 14 there are interim tests that are done from 9:00-10:00. These count for 5 %, 5 % and 10 %, respectively. They will be done online: the problems will be available in ANS before 9:00, and pictures/scans of the result should be uploaded before 10:30.
    The material for the interim test on December 3 is the part on SAT/SMT (first four lectures). The material for the interim test on December 17 is the part on information theory (next four lectures). The material for the interim test on January 14 is the part on program correctness (last four lectures). In the last lecture on January 12 more examples of invariants will be presented; there will be no questions on these at the last interim test.

    To download:

    General course introduction.

    Slides on SAT/SMT.

    Exercises: Practice set P1.

    Assignment 1, due December 3.

    Syllabus of Fundamentals of Informatics, from which Chapter 4 covers the material on Information Theory.

    Extra information on information theory on video.

    All further material on Information Theory, including slides, Practice sets P2a, P2b, P2c, and Assignment 2.

    Exercises: Practice set P3.

    Assignment 3, due January 14.

    Slides on program correctness . Note that the most recent version of 97 slides was uploaded on December 15.

    An example of a final examination .

    The final examination of January 2020.

    The final examination of April 2020. .

    The final examination of January 2021.

    The final examination of April 2021. .


    Lectures and topics:
    The numbers refer to the numbers of the video lectures, the dates indicate the online lectures. The recorded online lectures on information theory are available here, these on program correctness on Canvas > Files.
    number date lecturer topic material exercises
    1 Wednesday, November 17 Hans Zantema Introduction, SAT solving, SMT, SMTlib syntax, Z3, 8 queens problem SAT/SMT slides 1-46 P1: 1-6
    2 Friday, November 19 Hans Zantema generating SMT code, rectangle fitting, sudoku, CNF, resolution SAT/SMT slides 47-72, 80-88 P1: 7-9, 11
    3 Wednesday, November 24 Hans Zantema Resolution, proof systems, DPLL, scheduling example SAT/SMT slides 89-118, 73-79 P1: 10, 12-15
    4 Friday, November 26 Hans Zantema DPPL to resolution: resolution complete, Tseitin transformation SAT/SMT slides 119-143 P1: 16, 17
    5 Wednesday, December 1 Tom Verhoeff Measuring information Syllabus Ch.4 through §4.2, and §4.5 – §4.7 P2a: 1, 2, 4, 5; P2c: 1, 2
    6 Friday, December 3 Tom Verhoeff Efficiency by compression Syllabus §4.3 – §4.4 P2a: 3, 6, 7, 8, 9, 10; P2c: 3, 4
    7 Wednesday, December 8 Tom Verhoeff Reliability by error control Syllabus §4.8 – §4.13 P2b (all); P2c: 5, 6
    8 Friday, December 10 Tom Verhoeff Security by cryptography Syllabus §4.14 – §4.23 P2c: 7, 8, 9
    9 Wednesday, December 15 Hans Zantema Program Correctness: bounded model checking, basic rules in Hoare logic slides on program correctness 1-29 P3: 1-4
    10 Friday, December 17 Hans Zantema Hoare logic and wp calculus for assignment, composition and if-then-else, invariants slides on program correctness 30-53 P3: 5-8
    11 Wednesday, December 22 Hans Zantema Invariants, proof rule for while, fast multiplication, how to choose invariant slides on program correctness 54-77 P3: 9-15
    12 Wednesday, January 12 Hans Zantema Applications of invariants: binary search, graph algorithms slides on program correctness 78-97




    Last change: January 17, 2022