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ý, Václav Kůla, Jan Tóth
Course supervisor: Filip Železný
The materials from the previous iteration of this course are available here.
| Date | Lecturer | Topic | Resources | |
|---|---|---|---|---|
| 1 | 23.9. | Chvalovský | Introduction and propositional logic (recap) | slides |
| 2 | 30.9. | Chvalovský | SAT solving—resolution and DPLL | slides |
| 3 | 7.10. | Chvalovský | SAT solving—CDCL and probabilistic methods | slides |
| 4 | 14.10. | Chvalovský | SAT solving (cont'd), FOL, and SMT | slides |
| 5 | 21.10. | Chvalovský | SMT | slides |
| 6 | 28.10. | Statehood Day | no lecture | |
| 7 | 4.11. | Chvalovský | SMT (cont'd) and quantifiers in FOL | slides |
| 8 | 11.11. | Chvalovský | FOL—Resolution, Equality, and Model Finding | slides |
| 9 | 18.11. | Chvalovský | Proof assistants | slides |
| 10 | 25.11. | Kuželka | Introduction to Prolog | slides |
| 11 | 2.12. | Kuželka | Recursion, lists | slides (Erratum: In the example starting at ~17:30, there should be predicate connectedS instead of connected.) |
| 12 | 9.12. | Kuželka | SLD trees, cut, negation | slides |
| 13 | 16.12. | Kuželka | Search in Prolog | slides |
| 14 | 6.1. | Kuželka | Answer set programming | slides |
Videos for the Prolog part:
Lecture 10: 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}), Lecture 11:video (Erratum: In the example starting at ~17:30, we there should be predicate connectedS instead of connected.), Lecture 12: part 1, part 2, part 3, Lecture 13: video, Lecture 14:video (Notes: I apologize for the poor technical quality of the recordings. Slides in most of the videos are based on materials by Peter Flach.)
Note that the titles and topics of future lectures are tentative and subject to change.
| Date | Tutor | Topic | Resources | |
|---|---|---|---|---|
| 1 | 23.9. | Chvalovský | General discussion, propositional logic, and normal forms | exercises |
| 2 | 30.9. | Chvalovský | SAT Solving I | exercises |
| 3 | 7.10. | Chvalovský | SAT Solving II | exercises, notebooks |
| 4 | 14.10. | Chvalovský | SAT Solving III and FOL | exercises |
| 5 | 21.10. | Chvalovský | SMT | exercises, SMT files |
| 6 | 28.10. | Statehood Day | no labs | |
| 7 | 4.11. | Chvalovský | SMT (cont'd) and FOL (basic notions) | exercises |
| 8 | 11.11. | Chvalovský | FOL Resolution, ATPs | exercises, TPTP files |
| 9 | 18.11. | Chvalovský | Isabelle | exercises |
| 10 | 25.11. | Kůla | Prolog as a Database | exercises |
| 11 | 2.12. | Kůla | Lists in Prolog | exercises |
| 12 | 9.12. | Kůla | Cut in Prolog | exercises |
| 13 | 16.12. | Kůla | Search in Prolog | exercises |
| 14 | 6.1. | Kůla | Answer Set Programming | exercises |
Note that the titles and topics of future labs are tentative and subject to change.
There will be 3 tasks 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 three years ago, 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. An online book that covers various topics discussed in the course is Logic and Mechanized Reasoning. Yet another relevant book available from the CTU networks is Mathematical Logic for Computer Science.