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