Warning
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 if at least one student in the room is non-Czech.

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

Lecturers: Filip Železný and Karel Chvalovský

Lectures

Date Lecturer Topic Resources
1 23.9. Chvalovský Introduction and propositional logic (recap) slides
2 30.9. Chvalovský SAT solving—resolution, DPLL, and CDCL slides
3 7.10. Chvalovský SAT solving (cont'd) and introduction to SMT slides
4 14.10. Chvalovský Satisfiability modulo theories (SMT) slides
5 21.10. Železný Introduction to Prolog prolog-1.pptx
6 4.11. Železný Recursion, lists see above
7 11.11. Železný SLD trees, cut, negation prolog-2.ppt
8 18.11. Železný Search in Prolog prolog-3.ppt
9 25.11. Chvalovský Answer set programming slides
10 2.12. Chvalovský First-order logic slides
11 9.12. Chvalovský First-order resolution slides
12 16.12. Chvalovský Equality and model finding slides
13 6.1. Chvalovský Proof assistants slides

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 and exercises on propositional logic exercises
2 30.9. Chvalovský SAT solving exercises
3 7.10. Chvalovský SAT solving (cont'd) exercises
4 14.10. Chvalovský SAT solving (cont'd) and SMT exercises
5 21.10. Černoch Prolog as a database exercises
6 4.11. Černoch Lists in Prolog exercises
7 11.11. Černoch Search strategies exercises
8 18.11. Černoch Cut and arithmetics exercises
9 25.11. Chvalovský Answer set programming exercises
10 2.12. Chvalovský First-order logic exercises
11 9.12. Chvalovský First-order resolution exercises
12 16.12. Chvalovský Equality and theorem provers exercises
13 6.1. Chvalovský Proof assistants exercises

Tasks

Assigned Deadline Name BRUTE label Description Points
1 14.10. 11.11. Scheduling task1 20
2 2.12. 7.1. Prolog task2 15
3 16.12. 13.1. Modal logic task3 15

Grading

Labs

There will be 3 tasks (for 20, 15, and 15 points) assigned during the semester. You submit your solutions through UploadSystem. 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), see a sample, and to pass you need at least 25 points. You are eligible for a grade only after you receive the assessment for labs. 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

SAT/SMT

TPTP

Automated Theorem Provers

Model Finders

courses/lup/start.txt · Last modified: 2020/01/06 14:15 by chvalkar