Logical Reasoning and Programming
Code | Completion | Credits | Range | Language |
---|---|---|---|---|
BE4M36LUP | Z,ZK | 6 | 2P+2C | English |
- The course cannot be taken simultaneously with:
- Logical Reasoning and Programming (B4M36LUP)
- The course is a substitute for:
- Logical Reasoning and Programming (B4M36LUP)
- Garant předmětu:
- Filip Železný
- Lecturer:
- Karel Chvalovský, Ondřej Kuželka
- Tutor:
- Karel Chvalovský, Jan Tóth
- Supervisor:
- Department of Computer Science
- Synopsis:
-
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.
- Requirements:
- Syllabus of lectures:
-
1Introduction and propositional logic (recap)
2SAT solving—resolution, DPLL, and CDCL
3SAT solving (cont'd) and introduction to SMT
4Satisfiability modulo theories (SMT)
5Introduction to Prolog
6Recursion, lists
7SLD trees, cut, negation
8Search in Prolog
9Answer set programming
10First-order logic
11First-order resolution
12Equality and model finding
13Proof assistants
- Syllabus of tutorials:
- Study Objective:
- Study materials:
-
Bundy, A.: The Computational Modelling of Mathematical Reasoning, Academic Press 1983 (Bundy).
Clarke, E.M. Jr., Grumberg, O. and Peled, D. A.: Model Checking, The MIT Press, 1999, Fourth Printing 2002.
Newborn, M.: Automated Theorem Proving: Theory and Practice
Robinson, J.A., Voronkov, A. (Eds.): Handbook of Automated Reasoning (in 2 volumes). Elsevier and MIT Press 2001
Weidenbach, Ch.: SPASS: Combining Superposition, Sorts and Splitting (1999)
Wos, L. and Pieper, G.W.: A Fascinating Country in the World of Computing: Your Guide to Automated Reasoning
Flach P.: Simply Logical ? Intelligent Reasoning by Example, John Wiley, 1998
Bratko I.: Prolog Programming for Artificial Intelligence, Addison-Wesley, 2011
- Note:
- Further information:
- https://cw.fel.cvut.cz/b201/courses/lup/start
- Time-table for winter semester 2022/2023:
-
06:00–08:0008:00–10:0010:00–12:0012:00–14:0014:00–16:0016:00–18:0018:00–20:0020:00–22:0022:00–24:00
Mon Tue Wed Thu Fri - Time-table for summer semester 2022/2023:
- Time-table is not available yet
- The course is a part of the following study plans:
-
- Open Informatics - Artificial Intelligence (compulsory course of the specialization)