Information on the course

Applied Logic (2ITX0)

This is the information about the 5ects elective course Applied Logic 2ITX0.

Due to the covid-19 regulations the resit on April 17 will be held online: you get a pdf of the problems just before 18:00 and you should upload scans of your work in ANS no later than 21:30. After a first grading there may be short skype interviews with the students to discuss the work.
Instructions of how to download and upload in ANS is given in ANS instructions. It is recommended to do the indicated trial in advance.

The course grew out from the earlier course 2IS80 Fundamentals of Informatics. As it has a big overlap with 2IS80, it is not allowed to have 2IS80 and 2ITX0 in the same program.

The lecturers are

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 three ingredients: Assessment:
The course is concluded by a written examination that counts for 55 %. 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.

Due to the covid-19 regulations the resit on April 17 will be held online: you get a pdf of the problems in advance and you should upload scans of your work in ANS. Details will follow.

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

Apart from that there are three assignments that should be handed in electronically in the ANS system (via by every student individually, and count for 15 % each. The deadlines for these assignments are November 29, December 13 and January 10.

To download:

General course introduction.

Slides on SAT/SMT (this is a new version from November 20, 2019).

Exercises: Practice set P1.

Assignment 1, due November 29.

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 10.

Slides on program correctness .

An example of a final examination .

The final examination of January 2020. .

Lectures and topics:

date lecturer topic material exercises
Wednesday, November 13 Hans Zantema Introduction, SAT solving, SMT, SMTlib syntax, Z3, 8 queens problem SAT/SMT slides 1-46 P1: 1-6
Friday, November 15 Hans Zantema generating SMT code, rectangle fitting, sudoku, CNF, resolution SAT/SMT slides 47-72, 80-88 P1: 7-9, 11
Wednesday, November 20 Hans Zantema Resolution, proof systems, DPLL, scheduling example SAT/SMT slides 89-118, 73-79 P1: 10, 12-15
Friday, November 22 Hans Zantema DPPL to resolution: resolution complete, Tseitin transformation SAT/SMT slides 119-143 P1: 16, 17
Wednesday, November 27 Tom Verhoeff Measuring information Syllabus Ch.4 through 4.2, and 4.5 4.7 P2a: 1, 2, 4, 5; P2c: 1, 2
Friday, November 29 Tom Verhoeff : Efficiency by compression Syllabus 4.3 4.4 P2a: 3, 6, 7, 8, 9, 10; P2c: 3, 4
Wednesday, December 4 Tom Verhoeff Reliability by error control Syllabus 4.8 4.13 P2b (all); P2c: 5, 6
Friday, December 6 Tom Verhoeff Security by cryptography Syllabus 4.14 4.23 P2c: 7, 8, 9
Wednesday, December 11 Hans Zantema Program Correctness: bounded model checking, basic rules in Hoare logic slides on program correctness 1-29 P3: 1-4
Friday, December 13 Hans Zantema Hoare logic and wp calculus for assignment, composition and if-then-else, invariants slides on program correctness 30-53 P3: 5-8
Wednesday, December 18 Hans Zantema Invariants, proof rule for while, fast multiplication slides on program correctness 54-74 P3: 9-15
Friday, December 20 Hans Zantema Applications of invariants: binary search, graph algorithms slides on program correctness 75-94
Wednesday, January 8 Tom Verhoeff Algorithmic information theory (not for exam), last tutorial
Friday, January 10 Hans Zantema Answering questions, presenting example examination, last lab session (part SAT/SMT, program correctness)
Wednesday, January 15 Hans Zantema Results of Assignment 3
Friday, January 17 Tom Verhoeff Answering questions, presenting example examination (part information theory)

Last change: April 6, 2020