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ý, Václav Kůla, Jan Tóth

Course supervisor: Filip Železný

Lectures

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
3 7.10. Chvalovský SAT solving (cont'd)—CDCL
4 14.10. Chvalovský SAT solving (cont'd), FOL, and SMT
5 21.10. Chvalovský FOL and SMT
6 28.10. Statehood Day no lecture
7 4.11. Chvalovský SMT (cont'd) and quantifiers in FOL
8 11.11. Chvalovský FOL—Resolution
FOL—Equality and model finding
9 18.11. Chvalovský Proof assistants
10 25.11. Kuželka Introduction to Prolog
11 2.12. Kuželka Recursion, lists
12 9.12. Kuželka SLD trees, cut, negation
13 16.12. Kuželka Search in Prolog
14 6.1. Kuželka Answer set programming

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

Labs

Date Tutor Topic Resources
1 23.9. Chvalovský General discussion, propositional logic, and normal forms exercises
2 30.9. Chvalovský SAT Solving I
3 7.10. Chvalovský SAT Solving II
4 14.10. Chvalovský SAT Solving III and FOL
5 21.10. Chvalovský SMT
6 28.10. Statehood Day no labs
7 4.11. Chvalovský SMT (cont'd) and FOL (basic notions)
8 11.11. Chvalovský FOL Resolution, ATPs
9 18.11. Chvalovský Isabelle
10 25.11. Prolog as a Database
11 2.12. Lists in Prolog
12 9.12. Cut in Prolog
13 16.12. Search in Prolog
14 6.1. Answer Set Programming

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

Tasks

Assigned Deadline Name BRUTE label Description Points
1
2
3

Grading

Labs

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.

Examination

The exam will be a written test (50 points) 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.

SAT/SMT

TPTP

Automated Theorem Provers

Model Finders

courses/lup/start.txt · Last modified: 2024/09/23 13:30 by chvalkar