Logical Reasoning and Programming

Vztahy:

Předmět BE4M36LUP může při kontrole studijních plánů nahradit předmět B4M36LUP

Předmět BE4M36LUP nesmí být zapsán, je-li v témže semestru zapsán anebo již dříve absolvován předmět B4M36LUP (vztah je symetrický)

Předmět BE4M36LUP nesmí být zapsán, je-li v témže semestru zapsán anebo již dříve absolvován předmět B4M36LUP (vztah je symetrický)

Garant předmětu:

Přednášející:

Cvičící:

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 solvingresolution, 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

Pro tento předmět se rozvrh nepřipravuje

Předmět je součástí následujících studijních plánů:

• Open Informatics - Artificial Intelligence (povinný předmět oboru)