Popis předmětu - B4M36LUP
Přehled studia |
Přehled oborů |
Všechny skupiny předmětů |
Všechny předměty |
Seznam rolí |
Vysvětlivky
Návod
| B4M36LUP | Logické usuzování a programování | ||
|---|---|---|---|
| Role: | PO | Rozsah výuky: | 2P+2C |
| Katedra: | 13136 | Jazyk výuky: | CS |
| Garanti: | Železný F. | Zakončení: | Z,ZK |
| Přednášející: | Chvalovský K., Kuželka O. | Kreditů: | 6 |
| Cvičící: | Chvalovský K., Tóth J. | Semestr: | Z |
Webová stránka:
https://cw.fel.cvut.cz/wiki/courses/lup/startAnotace:
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.Osnovy 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 |
Osnovy cvičení:
Literatura:
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, 2011Požadavky:
Předmět je zahrnut do těchto studijních plánů:
| Plán | Obor | Role | Dop. semestr |
| MPOI7_2018 | Umělá inteligence | PO | 3 |
| Stránka vytvořena 14.11.2025 17:51:45, semestry: L/2025-6, Z/2026-7, L/2024-5, Z/2025-6, L/2026-7, připomínky k informační náplni zasílejte správci studijních plánů | Návrh a realizace: I. Halaška (K336), J. Novák (K336) |