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:
https://cw.fel.cvut.cz/wiki/courses/lup/startAnotation:
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 assistantsExercises outline:
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, 2011Requirements:
Subject is included into these academic programs:| Program | Branch | Role | Recommended semester |
| MPOI7_2018 | Artificial Intelligence | PO | 3 |
| Page updated 7.9.2024 11:54:46, semester: Z/2023-4, Z/2024-5, L/2023-4, Z/2025-6, L/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) |