Subject description - B4M36LUP

Summary of Study | Summary of Branches | All Subject Groups | All Subjects | List of Roles | Explanatory Notes               Instructions
B4M36LUP Logical Reasoning and Programming
Roles:PO Extent of teaching:2P+2C
Department:13136 Language of teaching:CS
Guarantors:Železný F. Completion:Z,ZK
Lecturers:Chvalovský K., Železný F. Credits:6
Tutors:Černoch R., Chvalovský K., Železný F. Semester:Z


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.

Course outlines:

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

Exercises outline:


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


Subject is included into these academic programs:

Program Branch Role Recommended semester
MPOI7_2016 Artificial Intelligence PO 3
MPOI7_2018 Artificial Intelligence PO 3

Page updated 6.8.2020 15:51:54, semester: Z,L/2020-1, L/2019-20, Send comments about the content to the Administrators of the Academic Programs Proposal and Realization: I. Halaška (K336), J. Novák (K336)