Code: BE4M36LUP Logical Reasoning and Programming
Lecturer: prof. Ing. Filip Železný Ph.D. Weekly load: 2P+2C Completion: A, EX
Department: 13136 Credits: 6 Semester: W
Description:
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.
Contents:
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
Recommended literature:
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

Abbreviations used:

Semester:

Mode of completion of the course:

Weekly load (hours per week):