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
• Guarantor: Mgr. Mikoláš Janota, Ph.D.; RNDr. Martin Suda, Ph.D.
• Teacher(s): Mgr. Mikoláš Janota, Ph.D.
• Class: M Mgr. MMIB; M Mgr. MMIB > Povinně volitelné; M Mgr. MSTR; M Mgr. MSTR > Povinně volitelné
• Classification: Mathematics > Algebra

Annotation

English

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.

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

Czech

Seznámení se základními myšlenkami a metodami využití matematické logiky k řešení výpočetních problémů: SAT-solving, constraint programming, automatické dokazování, formální verifikace. Důraz bude kladen také na získání praktické zkušenosti s vybranými softwarovými nástroji.

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

Literature

English

Handbook of Satisfiability (https://dl.acm.org/doi/book/10.5555/1550723)

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

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

Requirements to the exam

English

Will be specified later.

Last update: Bulín Jakub, RNDr., Ph.D. (19.11.2019)

Czech

Požadavky budou upřesněny.

Last update: Bulín Jakub, RNDr., Ph.D. (19.11.2019)

Syllabus

English

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.

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