Logo ČVUT
CZECH TECHNICAL UNIVERSITY IN PRAGUE
STUDY PLANS
2023/2024
UPOZORNĚNÍ: Jsou dostupné studijní plány pro následující akademický rok.

Logical Reasoning and Programming

Login to KOS for course enrollment Display time-table
Code Completion Credits Range Language
B4M36LUP Z,ZK 6 2P+2C Czech

It is not possible to register for the course B4M36LUP if the student is concurrently registered for or has already completed the course BE4M36LUP (mutually exclusive courses).

The requirement for course B4M36LUP can be fulfilled by substitution with the course BE4M36LUP.

It is not possible to register for the course B4M36LUP if the student is concurrently registered for or has previously completed the course BE4M36LUP (mutually exclusive courses).

Garant předmětu:
Filip Železný
Lecturer:
Karel Chvalovský, Ondřej Kuželka
Tutor:
Karel Chvalovský, Jan Tóth
Supervisor:
Department of Computer Science
Synopsis:

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.

Requirements:
Syllabus of lectures:

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

Syllabus of tutorials:
Study Objective:
Study materials:

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

Note:
Further information:
https://cw.fel.cvut.cz/wiki/courses/lup/start
Time-table for winter semester 2023/2024:
06:00–08:0008:00–10:0010:00–12:0012:00–14:0014:00–16:0016:00–18:0018:00–20:0020:00–22:0022:00–24:00
Mon
roomKN:E-126
Chvalovský K.
Kuželka O.

09:15–10:45
(lecture parallel1)
Karlovo nám.
Trnkova posluchárna K5
roomKN:E-310
Chvalovský K.
Tóth J.

14:30–16:00
(lecture parallel1
parallel nr.101)

Karlovo nám.
Lab K310 Linux
roomKN:E-310
Chvalovský K.
Tóth J.

16:15–17:45
(lecture parallel1
parallel nr.102)

Karlovo nám.
Lab K310 Linux
Tue
Wed
Thu
Fri
Time-table for summer semester 2023/2024:
Time-table is not available yet
The course is a part of the following study plans:
Data valid to 2024-03-27
Aktualizace výše uvedených informací naleznete na adrese https://bilakniha.cvut.cz/en/predmet4701206.html