SubjectsSubjects(version: 945)
Course, academic year 2023/2024
   Login via CAS
Computational Logic - NMAG535
Title: Výpočetní logika
Guaranteed by: Department of Algebra (32-KA)
Faculty: Faculty of Mathematics and Physics
Actual: from 2021
Semester: winter
E-Credits: 5
Hours per week, examination: winter s.:2/2, C+Ex [HT]
Capacity: unlimited
Min. number of students: unlimited
4EU+: no
Virtual mobility / capacity: no
State of the course: taught
Language: English, Czech
Teaching methods: full-time
Teaching methods: full-time
Guarantor: Mgr. Mikoláš Janota, Ph.D.
RNDr. Martin Suda, Ph.D.
Class: M Mgr. MMIB
M Mgr. MMIB > Povinně volitelné
M Mgr. MSTR > Povinně volitelné
Classification: Mathematics > Algebra
Annotation -
Last update: doc. Mgr. et Mgr. Jan Žemlička, Ph.D. (10.12.2018)
Introduction to basic ideas and methods of applying mathematical logic to solving computational problems: SAT- solving, constraint programming, automated theorem proving, formal verification. The course will also emphasize gaining practical experience with selected software tools.
Literature -
Last update: doc. Mgr. et Mgr. Jan Žemlička, Ph.D. (21.05.2021)

Handbook of Satisfiability (

Decision Procedures: An Algorithmic Point of View Book by Daniel Kroening and Ofer Strichman

The Calculus of Computation: Decision Procedures with Applications to Verification Textbook by Aaron R. Bradley and Zohar Manna

Handbook of Knowledge Representation: F. Van Harmelen, Vladimir Lifschitz, and Bruce Porter 2008 Elsevier

Handbook of Constraint Programming: F. Rossi, Peter Van Beek, and Toby Walsh 2006 Elsevier

Niklas Eén, Niklas Sörensson: An Extensible SAT-solver. SAT 2003: 502-518

Requirements to the exam -
Last update: RNDr. Jakub Bulín, Ph.D. (19.11.2019)

Will be specified later.

Syllabus -
Last update: doc. Mgr. et Mgr. Jan Žemlička, Ph.D. (21.05.2021)

Decision problems in propositional logic (Boolean Satisfiability, SAT). Examples of modeling using propositional logic. Algorithms for SAT. Decision problems in first-order logic. The Satisfiability Modulo Theories (SMT) problem. Problem encodings for SAT. Algorithms for SMT. Constraint Programming (CP): algorithms and modeling examples. Encodings for propositional logic. Answer Set Programming (ASP): algorithms and modeling examples. Relationship with propositional logic. Function and enumeration problems for SAT, SMT, ASP and CP: including optimization problems and over specified sets of constraints. Decision, function and enumeration problems with quantified propositional variables. Application examples.

Charles University | Information system of Charles University |