====== 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: [[mailto:karel.chvalovsky@cvut.cz|Karel Chvalovský]], [[mailto:kuzelon2@fel.cvut.cz|Ondřej Kuželka]] Lab instructors: [[mailto:karel.chvalovsky@cvut.cz|Karel Chvalovský]], [[mailto:cernorad@fel.cvut.cz|Radomír Černoch]] Course supervisor: [[mailto:zelezny@fel.cvut.cz|Filip Železný]] **Until further notice, the class is held online in this [[https://teams.microsoft.com/l/team/19%3a6f098b9746894c75b789ce7bddbe6e11%40thread.tacv2/conversations?groupId=1741ea3e-d01f-45ff-bd6c-89b3c4f1527b&tenantId=f345c406-5268-43b0-b19f-5862fa6833f8|MS Teams space]] and live meetings are in the regular lecture/lab timetable slots.** ===== Lectures ===== [[https://teams.microsoft.com/l/channel/19%3a13d0b99433e343ba973f40b8bca8c853%40thread.tacv2/Lectures?groupId=1741ea3e-d01f-45ff-bd6c-89b3c4f1527b&tenantId=f345c406-5268-43b0-b19f-5862fa6833f8|MS Teams Lecture Channel]] (inside the MS Teams space linked above). ^ ^ Date ^ Lecturer ^ Topic ^ Resources ^ | 1 | 21.9. | Chvalovský | Introduction and propositional logic (recap) | {{:courses:lup:lup1.pdf|slides}} | | 2 | 5.10. | Chvalovský | SAT solving---resolution and DPLL | {{:courses:lup:lup2.pdf|slides}} | | 3 | 12.10. | Chvalovský | SAT solving (cont'd)---CDCL | {{:courses:lup:lup3.pdf|slides}} | | 4 | 19.10. | Chvalovský | Satisfiability modulo theories (SMT) | {{:courses:lup:lup4c.pdf|slides}} | | 5 | 26.10. | Kuželka | Introduction to Prolog |{{:courses:lup:lup5.pptx|slides}} | | 6 | 2.11. | Kuželka | Recursion, lists | {{:courses:lup:lup6.pdf|slides}} | | 7 | 9.11. | Kuželka | SLD trees, cut, negation | {{:courses:lup:lup7.pdf|slides}} | | 8 | 16.11. | Kuželka | Search in Prolog | {{:courses:lup:lup8.pdf|slides}} | | 9 | 23.11. | Chvalovský | Answer set programming | {{:courses:lup:lup9.pdf|slides}} | | 10 | 30.11. | Chvalovský | First-order logic | {{:courses:lup:lup10.pdf|slides}} | | 11 | 7.12. | Chvalovský | First-order resolution | {{:courses:lup:lup11.pdf|slides}} | | 12| 14.12. | Chvalovský | Equality and model finding | {{:courses:lup:lup12.pdf|slides}} | | 13 | 4.1. | Chvalovský | Proof assistants | {{:courses:lup:lup13.pdf|slides}} | Note that the titles and topics of future lectures are tentative and subject to change. ===== Labs ===== ^ ^ Date ^ Tutor ^ Topic ^ Resources ^ | 1 | 21.9. | Chvalovský | General discussion and exercises on propositional logic | {{:courses:lup:lup1_labs.pdf|exercises}} | | 2 | 5.10. | Chvalovský | SAT solving | {{:courses:lup:lup2_labs.pdf|exercises}} | | 3 | 12.10. | Chvalovský | SAT solving | {{:courses:lup:lup3_labs.pdf|exercises}} | | 4 | 19.10. | Chvalovský | SMT solving | {{:courses:lup:lup4_labs.pdf|exercises}} | | 5 | 26.10. | Černoch | Prolog as a database | {{ :courses:lup:tut1.pdf|exercises}} | | 6 | 2.11. | Černoch | Recursion and lists | {{ :courses:lup:tut2.pdf|exercises}} | | 7 | 9.11. | Černoch | Efficient programming | {{ :courses:lup:tut3.pdf|exercises}} | | 8 | 16.11. | Černoch | Search | {{ :courses:lup:tut4.pdf|exercises}} | | 9 | 23.11. | Chvalovský | Answer Set Programming | {{:courses:lup:lup9_labs.pdf|exercises}} | | 10 | 30.11. | Chvalovský | First-order logic | {{:courses:lup:lup10_labs.pdf|exercises}} | | 11 | 7.12. | Chvalovský | First-order resolution | {{:courses:lup:lup11_labs.pdf|exercises}} | | 12 | 14.12. | Chvalovský | Equality and theorem provers | {{:courses:lup:lup12_labs.pdf|exercises}} | | 13 | 4.1. | Chvalovský | Proof assistants | {{:courses:lup:lup13_labs.pdf|exercises}} | ==== Tasks ==== ^ ^ Assigned ^ Deadline ^ Name ^ BRUTE label ^ Description ^ Points ^ | 1 | 21.10. | 25.11.| Shirokuro | | {{:courses:lup:task1.pdf|task1}} | 20 | | 2 | 16.11. | 13.12.| Escape from Zurg / Verbal arithmetics | | {{:courses:lup:task2.pdf|task2}} | 15 | | 3 | 14.12. | 18.1.| Hilbert proof systems | | {{:courses:lup:task3.pdf|task3}} | 15 | ===== Grading ===== ==== Labs ==== There will be 3 tasks (for 20, 15, and 15 points) assigned during the semester. You submit your solutions through [[http://cw.felk.cvut.cz/brute/|BRUTE]]. Late submissions are penalized. An assessment is awarded if you receive at least 25 points for all your solutions. ==== Examination ==== Due to the current coronavirus situation, the examination will take the form of an oral online exam (50 points) 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. You need a computer that is capable of running [[https://apps.google.com/meet/|Goog Meet]], including audio and video. You will be sat alone, remotely in a place of your choice, with your webcam turned on during the whole exam. Although it is allowed to use the course materials and other resources during the exam, the relatively tight time window makes it highly unlikely that you will have the time to do this to any great extent. Instead, you will do best if you approach the exam as you would normally. On the other hand, it is not allowed to communicate with other people or seek advice from them during the exam. The exam consists of two separate parts: * Prolog (15 points, 15 minutes), and * Automated reasoning (35 points, 20 minutes). You will receive the exact times of your slots (and Google Meet links) in advance. Generally speaking, the Prolog session starts at 10:00 and the Automated reasoning session at 13:00. \\ === Prolog === The Prolog part of the exam will test your knowledge of the material from the lectures and possibly also from the tutorials. You may be also asked to explain/write/fix simple Prolog programs (but mostly just a few lines of code due to the format of the exam).\\ \\ === Automated reasoning === This part will cover mostly the theory presented during lectures 1-4 and 9-13. However, you might be asked to demonstrate your knowledge of theory on simple examples or their parts. Hence you should also understand the examples solved during labs. \\ === Final note === We understand that this is a new exam situation for you (and us). Moreover, your current situation might require alternative arrangements. If this is the case, please, feel free to contact us as soon as possible. ==== Grade ==== 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 | ===== Links ===== ==== SAT/SMT ==== * [[http://satassociation.org/sat-smt-school.html|SAT/SMT Summer Schools]] * [[http://fmv.jku.at/picosat/| PicoSAT]] and [[https://pypi.org/project/pycosat/|pycosat]] * [[http://minisat.se/| MiniSat]] * [[http://smtlib.cs.uiowa.edu/|SMT-LIB]] * [[https://rise4fun.com/z3/tutorial| Getting Started with Z3: A Guide]] ==== TPTP ==== * [[http://www.tptp.org|The TPTP Problem Library]] for Automated Theorem Proving (Thousands of Problems for Theorem Provers) * [[http://www.tptp.org/cgi-bin/SystemOnTPTP|System on TPTP]] - online interface for ATPs ==== Automated Theorem Provers ==== * [[http://www.eprover.org/|E prover]] * [[https://vprover.github.io/|Vampire]] * [[http://www.cs.unm.edu/~mccune/prover9/|Prover 9]], the successor of [[http://www.cs.unm.edu/~mccune/otter/|Otter]] ==== Model Finders ==== * Paradox * {{:courses:lup:paradox.gz|compiled version 2.3 for linux}} * [[http://code.haskell.org/folkung/|version 2.3]] * [[http://www.cse.chalmers.se/~koen/code/folkung.tar.gz|experimental version 3]] from [[http://www.cse.chalmers.se/~koen/|author's web page]] * [[http://www.cs.unm.edu/~mccune/prover9/|Mace4]]