Logo ČVUT
CZECH TECHNICAL UNIVERSITY IN PRAGUE
STUDY PLANS
2019/2020

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
The course cannot be taken simultaneously with:
Logical reasoning and programming (BE4M36LUP)
Lecturer:
Filip Železný (guarantor), Karel Chvalovský
Tutor:
Filip Železný (guarantor), Radomír Černoch, Karel Chvalovský
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:

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

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:
Time-table for winter semester 2019/2020:
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.
Železný F.

11:00–12:30
(lecture parallel1)
Karlovo nám.
Trnkova posluchárna K5
roomKN:E-310
Chvalovský K.
Černoch R.

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

Karlovo nám.
Lab K310 Linux
roomKN:E-310
Chvalovský K.
Černoch R.

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

Karlovo nám.
Lab K310 Linux
Tue
Fri
Thu
Fri
Time-table for summer semester 2019/2020:
Time-table is not available yet
The course is a part of the following study plans:
Data valid to 2019-10-14
For updated information see http://bilakniha.cvut.cz/en/predmet4701206.html