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., Kuželka O. Credits:6
Tutors:Chvalovský K., Tóth J. Semester:Z

Web page:


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:

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

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_2018 Artificial Intelligence PO 3

Page updated 18.6.2024 17:51:23, semester: Z,L/2023-4, Z/2024-5, Send comments about the content to the Administrators of the Academic Programs Proposal and Realization: I. Halaška (K336), J. Novák (K336)