This page is located in archive.

be4m36lup -- Logical reasoning and programming


Date Lecturer Topic Resources
1 2.10. Chvalovský Introduction and propositional logic slides
2 9.10. Chvalovský SAT solving - resolution, DPLL, and CDCL slides
3 16.10. Chvalovský Introduction to logic programming and Prolog - history, facts, rules, queries, functors, lists, unification covered by Chapter 1 and partially by Chapter 2 of Flach's slides, unification
4 23.10. Chvalovský Logic programming - Herbrand models, minimal models, definite clauses, decidability Chapter 2 of Flach's slides
5 30.10. Chvalovský SLD resolution, cut, CWA, negation as failure Chapter 3 of Flach's slides
6 6.11. Chvalovský Second-order predicates, difference lists, meta-interpreters, searching space using different strategies, definite clause grammars (DCG) covered by Chapters 3, 5, 6, 7 of Flach's slides
7 13.11. Vyskočil First-Order Logic slides
8 20.11. Vyskočil Semantic Tableau slides
9 27.11. Vyskočil Model Finding Methods slides
10 4.12. Vyskočil Equality in FOL, Paramodulation, Subsumption slides
11 11.12. Vyskočil ANL Loop, Superposition Calculus ANL Loop superposition ATPs
12 18.12. Vyskočil Halting Problem, Gödel's First Incompleteness Theorem slides

Lectures on logic programming and Prolog mostly follow Flach's book Simply Logical. See an online version or this webpage.


Date Tutor Topic Resources
1 2.10. Chvalovský General discussion and exercises on propositional logic exercises
2 9.10. Chvalovský Resolution and a Sudoku solver using SAT exercises, sudoku.py from pycosat
3 16.10. Chvalovský Unification, Prolog - queries and lists unification, exercises
4 23.10. Chvalovský Prolog examples, Herbrand models exercises
5 30.10. Chvalovský Arithmetic in Prolog, accumulators, sorting. exercises
6 6.11. Chvalovský Some built-in predicates, dynamically changing predicates, difference lists, grammars. exercises
7 13.11. Vyskočil System on TPTP
8 20.11. Vyskočil Negation Normal Form, Prenex Normal Form translations in Prolog fof_manipulations leantap.txt
9 27.11. Vyskočil Computing Interpretations in Prolog fof_interpretation
10 4.12. Vyskočil Skolemization in Prolog skolemization
11 11.12. Vyskočil Subsumption in Prolog subsumption
12 18.12. Vyskočil Flattening Clauses in Prolog clause_to_shallow_clause_translation


Assigned Deadline Name BRUTE label Description
1 24.10. 21.11. Numberlink NL task1
2 13.11. 12.12. Tseytin Transformation TT task2
3 11.12. 20.12. LeanTAP Proof Extraction PE task3
4 18.12. 7.1. Tableau Proof Verification PV task4
5 5.1. 31.1. Modaltap MT task5



There will be 5 tasks (for 10 points each) assigned during the semester. You submit your solutions through UploadSystem. Late submissions are penalized.

An assessment is awarded if you submit a solution for every task and receive at least 25 points for all your solutions (note that only tasks for which you receive at least 6 points are counted).


The examination consists of two parts a Prolog part and a theoretical part. Students are eligible for a grade only after they receive the assessment for labs. However, they can still attend the exam. The maximal number of points you can receive for the exam is 50.

The Prolog part of the exam is on computers. You can either use your own computer (a preferable option), or one in a lab. You submit your solution through the BRUTE system in a same way as you submitted your tasks. During this part, it is strictly not allowed to use any means of comunication (like social networks, emails, sms, …). On the other hand, you can use your notes and any other documentation.

The theoretical part is in a written form. Computers and any other materials are not allowed for this part.

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


Automated Theorem Provers

Model Finders

courses/be4m36lup/start.txt · Last modified: 2018/01/16 11:27 by vyskoji1