====== 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: [[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ý]] ===== Lectures ===== ^ ^ Date ^ Lecturer ^ Topic ^ Resources ^ | 1 | 20.9. | Chvalovský | Introduction and propositional logic (recap) | {{:courses:lup:lup1.pdf|slides}} | | 2 | 27.9. | Chvalovský | SAT solving---resolution and DPLL | {{:courses:lup:lup2.pdf|slides}} | | 3 | 4.10. | Chvalovský | SAT solving (cont'd)---CDCL | {{:courses:lup:lup3.pdf|slides}} | | 4 | 11.10. | Chvalovský | SAT solving (cont'd) | {{:courses:lup:lup4.pdf|slides}} | | 5 | 18.10. | Chvalovský | FOL and SMT | {{:courses:lup:lup5c.pdf|slides}} | | 6 | 25.10. | Chvalovský | SMT (cont'd) and quantifiers in FOL | {{:courses:lup:lup6.pdf|slides}}| | 7 | 1.11. | Chvalovský | First-Order Logic---Resolution | {{:courses:lup:lup7.pdf|slides}} | | 8 | 8.11. | Chvalovský | Resolution, equality, and model finding | {{:courses:lup:lup8.pdf|slides}} | | 9 | 15.11. | Chvalovský | Proof assistants | {{:courses:lup:lup9.pdf|slides}} | | 10 | 22.11. | Kuželka | Introduction to Prolog | {{:courses:lup:prolog1_2021.pdf|slides}} | | 11 | 29.11. | Kuželka | Recursion, lists | {{:courses:lup:prolog2_2021.pdf|slides}} | | 12| 6.12. | Kuželka | SLD trees, cut, negation | {{:courses:lup:prolog3_2021.pdf|slides}} | | 13 | 12.12. | Kuželka | Search in Prolog | {{:courses:lup:prolog4_2021.pdf|slides}} | | 14 | 3.1. | Kuželka | Answer set programming | {{:courses:lup:answer_set_programming_2021.pdf|slides}} | Note that the titles and topics of future lectures are tentative and subject to change. ===== Labs ===== ^ ^ Date ^ Tutor ^ Topic ^ Resources ^ | 1 | 20.9. | Chvalovský | General discussion and exercises on propositional logic | {{:courses:lup:lup1_labs.pdf|exercises}} | | 2 | 27.9. | Chvalovský | SAT Solving I | {{:courses:lup:lup2_labs.pdf|exercises}} | | 3 | 4.10. | Chvalovský | SAT Solving II | {{:courses:lup:lup3_labs.pdf|exercises}} | | 4 | 11.10. | Chvalovský | SAT Solving III | {{:courses:lup:lup4_labs.pdf|exercises}},\\ {{:courses:lup:lup4_labs_notebooks.tar.gz|notebooks}} | | 5 | 18.10. | Chvalovský | FOL and SMT | {{:courses:lup:lup5_labs.pdf|exercises}} | | 6 | 25.10. | Chvalovský | SMT (cont'd) and FOL (basic notions) | {{:courses:lup:lup6_labs.pdf|exercises}},\\ {{:courses:lup:lup6_labs_smt.tar.gz|smt problems}} | | 7 | 1.11. | Chvalovský | FOL and resolution | {{:courses:lup:lup7_labs.pdf|exercises}} | | 8 | 8.11. | Chvalovský | Resolution and ATPs | {{:courses:lup:lup8_labs.pdf|exercises}},\\ {{:courses:lup:lup8_labs.tar.gz|TPTP problems}} | | 9 | 15.11. | Chvalovský | Isabelle | {{:courses:lup:lup9_labs.pdf|exercises}} | | 10 | 22.11. | Černoch | Prolog as a database | {{ :courses:lup:lup10_labs.pdf|exercises}} | | 11 | 29.11. | Černoch | Lists in Prolog | {{ :courses:lup:lup11_labs.pdf|exercises}} | | 12 | 6.12. | Černoch | Cut in Prolog | {{ :courses:lup:lup12_labs.pdf|exercises}},\\ [[https://drive.google.com/file/d/1LgQkrNwKld77QDHAiV0LTljDEYaoya8H/view|recording]], \\ [[https://docs.google.com/document/d/172cGtPCxIVGZ5OcQSVr0Dce8JZBzgqe9p1Pw85mpdPE/edit|whiteboard 1]],\\ [[https://docs.google.com/document/d/1KLOOOLDiV3hW1BX-gvFNsAKbacsWHAQcjWiDVMp8W_c/edit|whiteboard 2]] | | 13 | 13.12. | Černoch | Search in Prolog | {{ :courses:lup:lup13_labs.pdf|exercises}}, \\ [[https://meet.google.com/xvx-uvde-oug|teleconference]], \\ [[https://docs.google.com/document/d/1VBVwqBcfYxEdWErckk76qalfU9JmsZ3uzFiNF5dlCao/edit|whiteboard 1]], \\ [[https://docs.google.com/document/d/1AvHu-ja18Aa8bdM1tKcEMpWs4Bzf7KLmttlpil84ivY/edit|whiteboard 2]] | | 14 | 20.9. | Kuželka | Answer set programming - continuing the lecture + exercises | [[https://cw.fel.cvut.cz/b201/_media/courses/lup/lup9_labs.pdf|excercises from last year (by K. Chvalovský)]] | ==== Tasks ==== ^ ^ Assigned ^ Deadline ^ Name ^ BRUTE label ^ Description ^ Points ^ | 1 | 13.10. | 11.11. | Light Up | | {{:courses:lup:task1.pdf|task1}} | 20 | | 2 | 15.11. | 14.12. | Proof systems | | {{:courses:lup:task2.pdf|task2}} | 15 | | 3 | 22.11. | 2.1. | Prolog search | | {{ :courses:lup:task3.pdf|task3}} | 15 | ===== Grading ===== //Note that although we all hope for the best, it may happen that we will have to adjust the following requirements to the evolving coronavirus situation.// ==== 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 ==== The exam will be a written test (50 points), see a {{:courses:lup:sample.pdf|sample}}, 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 | ===== Links ===== There are many general introductions covering basic notions from propositional and first-order logic. For example, the [[https://openlogicproject.org/|Open Logic Project]] is freely accessible. [[https://link.springer.com/book/10.1007%2F978-3-662-50497-0|Decision Procedures]] (PDF is available from the CTU network) covers many topics from SAT and SMT. Another relevant book available from the CTU networks is [[https://link.springer.com/book/10.1007/978-1-4471-4129-7|Mathematical Logic for Computer Science]]. ==== SAT/SMT ==== * [[http://satassociation.org/sat-smt-school.html|SAT/SMT Summer Schools]] * [[https://simons.berkeley.edu/programs/sat2021|Satisfiability: Theory, Practice, and Beyond]]---[[https://simons.berkeley.edu/|Simons Institute]] organized a bootcamp and many workshop on SAT (50th anniversary of Cook's paper) * [[https://simons.berkeley.edu/talks/sat-solving|SAT-solving using SATCH by Armin Biere]] * [[http://fmv.jku.at/picosat/| PicoSAT]] and [[https://pypi.org/project/pycosat/|pycosat]] * [[https://pysathq.github.io/|PySAT]] * [[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]]