====== be4m36lup -- Logical reasoning and programming ====== ===== Lectures ===== ^ ^ Date ^ Lecturer ^ Topic ^ Resources ^ | 1 | 2.10. | Chvalovský | Introduction and propositional logic | {{:courses:be4m36lup:lup1.pdf|slides}} | | 2 | 9.10. | Chvalovský | SAT solving - resolution, DPLL, and CDCL | {{:courses:be4m36lup:lup2.pdf|slides}} | | 3 | 16.10. | Chvalovský | Introduction to logic programming and Prolog - history, facts, rules, queries, functors, lists, unification | covered by {{:courses:be4m36lup:slchapter1.pdf|Chapter 1}} and partially by {{:courses:be4m36lup:slchapter2.pdf|Chapter 2}} of Flach's slides, {{:courses:be4m36lup:lup3-unification.pdf|unification}} | | 4 | 23.10. | Chvalovský | Logic programming - Herbrand models, minimal models, definite clauses, decidability | {{:courses:be4m36lup:slchapter2.pdf|Chapter 2}} of Flach's slides| | 5 | 30.10. | Chvalovský | SLD resolution, cut, CWA, negation as failure | {{:courses:be4m36lup:slchapter3.pdf|Chapter 3}} of Flach's slides| | 6 | 6.11. | Chvalovský | Second-order predicates, difference lists, meta-interpreters, searching space using different strategies, definite clause grammars (DCG) | covered by Chapters {{:courses:be4m36lup:slchapter3.pdf|3}}, {{:courses:be4m36lup:slchapter5.pdf|5}}, {{:courses:be4m36lup:slchapter6.pdf|6}}, {{:courses:be4m36lup:slchapter7.pdf|7}} of Flach's slides| | 7 | 13.11. | Vyskočil | First-Order Logic | {{:courses:be4m36lup:fol.pdf|slides}} | | 8 | 20.11. | Vyskočil | Semantic Tableau | {{:courses:be4m36lup:tableaux.pdf|slides}} | | 9 | 27.11. | Vyskočil | Model Finding Methods | {{:courses:be4m36lup:model_finding_methods.pdf|slides}} | | 10 | 4.12. | Vyskočil | Equality in FOL, Paramodulation, Subsumption |{{:courses:be4m36lup:resolution.pdf|slides}} | | 11 | 11.12. | Vyskočil | ANL Loop, Superposition Calculus | {{:courses:be4m36lup:ANL_loop.pdf|ANL Loop}} [[http://www.ii.uni.wroc.pl/~nivelle/teaching/special_atp/atp2007/superposition.pdf|superposition]] [[http://www.ii.uni.wroc.pl/~nivelle/teaching/special_atp/atp2007/reader.pdf|ATPs]]| | 12 | 18.12. | Vyskočil | Halting Problem, Gödel's First Incompleteness Theorem | {{:courses:be4m36lup:limits.pdf|slides}} | Lectures on logic programming and Prolog mostly follow Flach's book Simply Logical. See an [[http://book.simply-logical.space/|online version]] or [[https://www.cs.bris.ac.uk/~flach/SimplyLogical.html|this]] webpage. ===== Labs ===== ^ ^ Date ^ Tutor ^ Topic ^ Resources ^ | 1 | 2.10. | Chvalovský | General discussion and exercises on propositional logic | {{:courses:be4m36lup:lup1_labs.pdf|exercises}} | | 2 | 9.10. | Chvalovský | Resolution and a Sudoku solver using SAT | {{:courses:be4m36lup:lup2_labs.pdf|exercises}}, {{:courses:be4m36lup:sudoku.py|sudoku.py}} from pycosat | | 3 | 16.10. | Chvalovský | Unification, Prolog - queries and lists | {{:courses:be4m36lup:lup3-unification.pdf|unification}}, {{:courses:be4m36lup:lup3_labs.pdf|exercises}} | | 4 | 23.10. | Chvalovský | Prolog examples, Herbrand models | {{:courses:be4m36lup:lup4_labs.pdf|exercises}} | | 5 | 30.10. | Chvalovský | Arithmetic in Prolog, accumulators, sorting. | {{:courses:be4m36lup:lup5_labs.pdf|exercises}} | | 6 | 6.11. | Chvalovský | Some built-in predicates, dynamically changing predicates, difference lists, grammars. | {{:courses:be4m36lup:lup6_labs.pdf|exercises}} | | 7 | 13.11. | Vyskočil | System on TPTP | | | 8 | 20.11. | Vyskočil | Negation Normal Form, Prenex Normal Form translations in Prolog | {{:courses:be4m36lup:fof_manipulations.txt|fof_manipulations}} {{:courses:a4m33au:leantap.txt|}} | | 9 | 27.11. | Vyskočil | Computing Interpretations in Prolog | {{:courses:be4m36lup:fof_interpretation.txt|fof_interpretation}} | | 10 | 4.12. | Vyskočil | Skolemization in Prolog | {{:courses:be4m36lup:skolemization.txt|skolemization}} | | 11 | 11.12. | Vyskočil | Subsumption in Prolog | {{:courses:be4m36lup:subsumption.txt|subsumption}} | | 12 | 18.12. | Vyskočil | Flattening Clauses in Prolog | {{:courses:be4m36lup:clause_to_shallow_clause_translation.txt|clause_to_shallow_clause_translation}} | ==== Tasks ==== ^ ^ Assigned ^ Deadline ^ Name ^ BRUTE label ^Description ^ | 1 | 24.10. | 21.11. | Numberlink | NL | {{:courses:be4m36lup:task1.pdf|task1}} | | 2 | 13.11. | 12.12. | Tseytin Transformation | TT | {{:courses:be4m36lup:task2.pdf|task2}} | | 3 | 11.12. | 20.12. | LeanTAP Proof Extraction | PE | {{:courses:be4m36lup:task3.pdf|task3}} | | 4 | 18.12. | 7.1. | Tableau Proof Verification | PV | {{:courses:be4m36lup:task4.pdf|task4}} | | 5 | 5.1. | 31.1. | Modaltap | MT | {{:courses:be4m36lup:task5.pdf|task5}} | ===== Grading ===== ==== Labs ==== There will be 5 tasks (for 10 points each) assigned during the semester. You submit your solutions through [[http://cw.felk.cvut.cz/upload/|UploadSystem]]. Late submissions are penalized. An assessment is awarded if you submit a solution for every task and receive at least 25 points for all your solutions (note that only tasks for which you receive at least 6 points are counted). ==== Examination ==== The examination consists of two parts a Prolog part and a theoretical part. Students are eligible for a grade only after they receive the assessment for labs. However, they can still attend the exam. The maximal number of points you can receive for the exam is 50. The Prolog part of the exam is on computers. You can either use your own computer (a preferable option), or one in a lab. You submit your solution through the BRUTE system in a same way as you submitted your tasks. During this part, it is strictly not allowed to use any means of comunication (like social networks, emails, sms, ...). On the other hand, you can use your notes and any other documentation. The theoretical part is in a written form. Computers and any other materials are not allowed for this part. 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 ===== ==== TPTP ==== * [[http://www.tptp.org|The TPTP Problem Library]] for Automated Theorem Proving (Thousands of * Problems for Theorem Provers) * [[http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTP|System on TPTP]] - online interface for ATPs ==== Automated Theorem Provers ==== * [[http://www.eprover.org/|E prover]] * [[http://www.vprover.org/|Vampire]] * [[http://www.cs.unm.edu/~mccune/prover9/|Prover 9]], the successor of [[http://www.cs.unm.edu/~mccune/otter/|Otter]] * [[http://deepthought.ttu.ee/it/gandalf/|Gandalf]] * {{:courses:a4m33au:leantap.txt|LeanTAP}} ==== Model Finders ==== * Paradox * [[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]]