This page is located in archive. Go to the latest version of this course pages. Go the latest version of this page.

LUP – Logical reasoning and programming

This page provides information for the class B4M36LUP - Logické usuzování a programování as well as its English-language counterpart BE4M36LUP - Logical reasoning and programming, which are taught jointly. The lectures are held in English unless all participants speak Czech.

The course's aim is to explain selected significant methods of computational logic. These include algorithms for propositional satisfiability checking, first-order theorem proving and model-finding, and logical programming in Prolog,. Time permitting, we will also discuss some complexity and decidability issues pertaining to the said methods.

Lecturers: Karel Chvalovský, Ondřej Kuželka

Lab instructors: Karel Chvalovský, Jan Tóth

Course supervisor: Filip Železný


Date Lecturer Topic Resources
1 19.9. Chvalovský Introduction and propositional logic (recap) slides
2 26.9. Chvalovský SAT solving—resolution and DPLL slides
3 3.10. Chvalovský SAT solving (cont'd)—CDCL slides
4 10.10. Chvalovský SAT solving (cont'd), FOL, and SMT slides
5 17.10. Chvalovský FOL and SMT slides
6 24.10. Chvalovský SMT (cont'd) and quantifiers in FOL slides
7 31.10. Chvalovský First-Order Logic—Resolution slides
8 7.11. Chvalovský Resolution, equality, and model finding slides
9 14.11. Chvalovský Proof assistants slides
10 21.11. Kuželka Introduction to Prolog slides, videos: part 1, part 2, part 3 (Erratum: On the slide “An Example (2)” in part 3, the Herbrand universe should be {maria, peter, ai_techniques})
11 28.11. Kuželka Recursion, lists slides, video (Erratum: In the example starting at ~17:30, we there should be predicate connectedS instead of connected.)
12 5.12. Kuželka SLD trees, cut, negation slides, videos: part 1, part 2, part 3 (Note: Slides mostly based on materials by Peter Flach.)
13 12.12. Kuželka Search in Prolog slides, video
14 9.1. Kuželka Answer set programming slides, video

Note that the titles and topics of future lectures are tentative and subject to change.


Date Tutor Topic Resources
1 19.9. Chvalovský General discussion and exercises on propositional logic exercises
2 26.9. Chvalovský SAT Solving I exercises
3 3.10. Chvalovský SAT Solving II exercises,
4 10.10. Chvalovský SAT Solving III and FOL exercises
5 17.10. Chvalovský SMT exercises
SMT examples
6 24.10. Chvalovský SMT (cont'd) and FOL (basic notions) exercises
7 31.10. Chvalovský FOL (resolution) exercises
TPTP examples
8 7.11. Chvalovský Resolution ant ATPs exercises
TPTP examples
9 14.11. Chvalovský Isabelle exercises
10 21.11. Tóth Prolog as a Database exercises
11 28.11. Tóth Lists in Prolog exercises
12 5.12. Tóth Arithemtics and Cut in Prolog exercises
13 12.12. Tóth Search in Prolog exercises
14 9.1. Tóth Answer Set Programming exercises


Assigned Deadline Name BRUTE label Description Points
1 17.10. 14.11. Shirokuro task1 20
2 14.11. 12.12. Proof systems task2 15
3 12.12. 31.1. Puzzles in Prolog prolog task3 15


Note that although we all hope for the best, it may happen that we will have to adjust the following requirements to the evolving coronavirus situation.


There will be 3 tasks (for 20, 15, and 15 points) assigned during the semester. You submit your solutions through BRUTE. Late submissions are penalized.

An assessment is awarded if you receive at least 25 points for all your solutions.


The exam will be a written test (50 points), see a sample and a test from last year, and to pass, you need to get at least 25 points. You are eligible for a grade only after receiving the labs assessment. However, you can still attend the exam.

The final grade is based on the sum of points you receive for labs (max. 50 pts.) and the exam (max. 50 pts.) and follows university regulations:

Points Grade
100-90 A 1 excellent
89-80 B 1.5 very good
79-70 C 2 good
69-60 D 2.5 satisfactory
59-50 E 3 sufficient
<50 F 4 failed

There are many general introductions covering basic notions from propositional and first-order logic. For example, the Open Logic Project is freely accessible. Decision Procedures (PDF is available from the CTU network) covers many topics from SAT and SMT. Another relevant book available from the CTU networks is Mathematical Logic for Computer Science.



Automated Theorem Provers

Model Finders

courses/lup/start.txt · Last modified: 2023/02/01 14:34 by tothjan2