Logo ČVUT
ČESKÉ VYSOKÉ UČENÍ TECHNICKÉ V PRAZE
STUDIJNÍ PLÁNY
2022/2023
UPOZORNĚNÍ: Jsou dostupné studijní plány pro následující akademický rok.

Logical Reasoning and Programming

Přihlášení do KOSu pro zápis předmětu Zobrazit rozvrh
Kód Zakončení Kredity Rozsah Jazyk výuky
BE4M36LUP Z,ZK 6 2P+2C anglicky
Předmět nesmí být zapsán současně s:
Logické usuzování a programování (B4M36LUP)
Předmět je náhradou za:
Logické usuzování a programování (B4M36LUP)
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:

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

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/b201/courses/lup/start
Rozvrh na zimní semestr 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
Po
místnost KN:E-126
Chvalovský K.
Kuželka O.

09:15–10:45
(přednášková par. 1)
Karlovo nám.
Trnkova posluchárna K5
místnost KN:E-310
Chvalovský K.
Tóth J.

14:30–16:00
(přednášková par. 1
paralelka 101)

Karlovo nám.
Lab K310 Linux
Út
St
Čt

Rozvrh na letní semestr 2022/2023:
Rozvrh není připraven
Předmět je součástí následujících studijních plánů:
Platnost dat k 29. 5. 2023
Aktualizace výše uvedených informací naleznete na adrese https://bilakniha.cvut.cz/cs/predmet4869806.html