Logo ČVUT
ČESKÉ VYSOKÉ UČENÍ TECHNICKÉ V PRAZE
STUDIJNÍ PLÁNY
2019/2020

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
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)
Přednášející:
Filip Železný (gar.), Karel Chvalovský
Cvičící:
Filip Železný (gar.), Radomír Černoch, Karel Chvalovský
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, propositional logic, and SAT

2 SAT solving - resolution, DPLL, and CDCL

3 Prolog

4 Prolog

5 Prolog

6 Prolog

7 Answer set programming

8 First-order logic and semantic tableaux

9 Model finding methods

10 Resolution and equality in FOL

11 ANL loop, superposition calculus

12 Proof assistants

13 Complexity and decidability issues, SMT

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:
Rozvrh na zimní semestr 2019/2020:
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.
Železný F.

11:00–12:30
(přednášková par. 1)
Karlovo nám.
Trnkova posluchárna K5
místnost KN:E-310
Chvalovský K.
Černoch R.

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

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

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