====== 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:zelezny@fel.cvut.cz|Filip Železný]] and [[mailto:Karel.Chvalovsky@cvut.cz|Karel Chvalovský]] 
===== Lectures =====
^ ^ Date ^  Lecturer ^ Topic ^ Resources ^
|  1 | 1.10. |  Chvalovský | Introduction, propositional logic, and SAT | {{:courses:lup:lup1.pdf|slides}} |
|  2 | 8.10. |  Chvalovský | SAT solving - resolution, DPLL, and CDCL | {{:courses:lup:lup2.pdf|slides}} |
|  3 | 15.10. |  Železný | Introduction to Prolog | {{:courses:lup:Prolog-1.pptx|slides}} |
|  4 | 22.10. |  Železný | Prolog: SLD trees, cuts | {{:courses:lup:prolog-2.ppt|slides}} |
|  5 | 29.10. |  Železný | Prolog: search algorithms | {{:courses:lup:prolog-3.ppt|slides}} |
|  6 | 5.11. |  Železný | Prolog (search algos cont'd) | |
|  7 | 12.11. |  Chvalovský | Answer set programming | {{:courses:lup:lup7.pdf|slides}} |
|  8 | 19.11. |  Chvalovský | First-order logic | {{:courses:lup:lup8.pdf|slides}} |
|  9 | 26.11. |  Chvalovský | First-order resolution | {{:courses:lup:lup9.pdf|slides}} |
| 10 |  3.12. |  Chvalovský | First-order resolution and equality | {{:courses:lup:lup10.pdf|slides}} |
| 11 | 10.12. |  Chvalovský | First-order tableaux and model finding | {{:courses:lup:lup11.pdf|slides}} |
| 12 | 17.12. | Chvalovský | Complexity and decidability issues, SMT  | {{:courses:lup:lup12c.pdf|slides}} |
| 13 | 7.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 |   1.10. |  Chvalovský | General discussion and exercises on propositional logic | {{:courses:lup:lup1_labs.pdf|exercises}} |
|  2 |   8.10. |  Chvalovský | Resolution and SAT solving | {{:courses:lup:lup2_labs.pdf|exercises}} |
|  3 |  15.10. |     Černoch | Prolog as a database | {{:courses:lup:tut1.pdf|exercises}} |
|  4 |  22.10. |     Černoch | Lists in Prolog | {{:courses:lup:tut2.pdf|exercises}} |
|  5 |  29.10. |     Černoch | Efficient proramming in Prolog | {{:courses:lup:tut3.pdf|exercises}} |
|  6 |   5.11. |     Černoch | Search strategies | {{:courses:lup:tut4.pdf|exercises}} |
|  7 |  12.11. |  Chvalovský | Answer set programming | {{:courses:lup:lup7_labs.pdf|exercises}} |
|  8 |  19.11. |  Chvalovský | First-order logic semantics | {{:courses:lup:lup8_labs.pdf|exercises}} |
|  9 |  26.11. |  Chvalovský | First-order logic transformations | {{:courses:lup:lup9_labs.pdf|exercises}} |
|  10 |  3.12. |  Chvalovský | First-order resolution and TPTP | {{:courses:lup:lup10_labs.pdf|exercises}} |
|  11 | 10.12. |  Chvalovský | First-order proving and model finding | {{:courses:lup:lup11_labs.pdf|exercises}} |
|  12 | 17.12. |  Chvalovský | First-order tableaux and SMT | {{:courses:lup:lup12_labs.pdf|exercises}} |
|  12 | 17.12. |  Chvalovský | Proof assistants (Isabelle) | {{:courses:lup:lup13_labs.pdf|exercises}} |


==== Tasks ====
^  ^ Assigned ^ Deadline ^ Name           ^ BRUTE label ^ Description                  ^ Points ^
|  1 |   8.10. |  29.10. | Light Up               | LU  | {{:courses:lup:task1.pdf|task1}} | 20 |
|  2 |  13.11. |   5.12. | Term Rewriting Systems | TRS | {{:courses:lup:trs.pdf|task2}}   | 15 | 
|  3 |  11.12. |    8.1. | Modal logic            | ML  | {{: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/upload/|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 {{:courses:lup:sample.pdf|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  |

===== 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]]

==== 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]]