Logické usuzování a programování
Kód | Zakončení | Kredity | Rozsah | Jazyk výuky |
---|---|---|---|---|
B4M36LUP | Z,ZK | 6 | 2P+2C | česky |
- Vztahy:
- Předmět B4M36LUP nesmí být zapsán, je-li v témže semestru zapsán anebo již dříve absolvován předmět BE4M36LUP (vztah je symetrický)
- Předmět B4M36LUP může být splněn v zastoupení předmětem BE4M36LUP
- Předmět B4M36LUP nesmí být zapsán, je-li v témže semestru zapsán anebo již dříve absolvován předmět BE4M36LUP (vztah je symetrický)
- Garant předmětu:
- Filip Železný
- Přednášející:
- Karel Chvalovský, Ondřej Kuželka
- Cvičící:
- Karel Chvalovský, Jan Tóth
- Předmět zajišťuje:
- katedra počítačů
- Anotace:
-
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.
- Požadavky:
- Osnova přednášek:
-
1.Introduction and propositional logic (recap)
2.SAT solving—resolution, DPLL, and CDCL
3.SAT solving (cont'd) and introduction to SMT
4.Satisfiability modulo theories (SMT)
5.Introduction to Prolog
6.Recursion, lists
7.SLD trees, cut, negation
8.Search in Prolog
9.Answer set programming
10.First-order logic
11.First-order resolution
12.Equality and model finding
13.Proof assistants
- Osnova cvičení:
- Cíle studia:
- Studijní materiály:
-
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
- Poznámka:
- Další informace:
- https://cw.fel.cvut.cz/wiki/courses/lup/start
- Rozvrh na zimní semestr 2024/2025:
-
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
Po Út St Čt Pá - Rozvrh na letní semestr 2024/2025:
- Rozvrh není připraven
- Předmět je součástí následujících studijních plánů:
-
- Otevřená informatika - Umělá inteligence 2018 (povinný předmět oboru)