FI:IA085 SAT and Automated Reasoning - Informace o předmětu
IA085 Satisfiability and Automated Reasoning
Fakulta informatikyjaro 2026
- Rozsah
- 2/1/1. 4 kr. (plus ukončení). Ukončení: zk.
Vyučováno kontaktně - Vyučující
- RNDr. Martin Jonáš, Ph.D. (přednášející)
Mgr. Jakub Šárník (cvičící) - Garance
- RNDr. Martin Jonáš, Ph.D.
Katedra teorie programování – Fakulta informatiky
Dodavatelské pracoviště: Katedra teorie programování – Fakulta informatiky - Rozvrh
- Út 17. 2. až Út 12. 5. Út 14:00–15:50 C408
- Rozvrh seminárních/paralelních skupin:
- Omezení zápisu do předmětu
- Předmět je otevřen studentům libovolného oboru.
- Anotace
- At the end of the course, students should:
- have working knowledge of propositional logic and first-order logic,
- be able to express real-world problems in a suitable logical formalism,
- be able to explain principles, algorithms, and underlying theoretical concepts of modern satisfiability solvers and theorem provers,
- be able to assess what kind of tool is relevant for their problem and apply an existing satisfiability solver or theorem prover to the problem,
- understand strengths and weaknesses of existing satisfiability solvers and theorem provers. - Výstupy z učení
- At the end of the course, students should:
- have working knowledge of propositional logic and first-order logic,
- be able to express real-world problems in a suitable logical formalism,
- be able to explain principles, algorithms, and underlying theoretical concepts of modern satisfiability solvers and theorem provers,
- be able to assess what kind of tool is relevant for their problem and apply an existing satisfiability solver or theorem prover to the problem,
- understand strengths and weaknesses of existing satisfiability solvers and theorem provers. - Klíčová témata
- Propositional satisfiability: syntax and semantics of propositional logic , encoding of real-world problems, historical and modern satisfiability decision procedures, design and usage of modern satisfiability solvers, preprocessing techniques, proofs of unsatisfiability.
- Satisfiability Modulo Theories: syntax and semantics of first-order logic without quantifiers; first-order theories relevant for description of systems, their decidability and complexity; CDCL(T) algorithm and theory solvers for selected first-order theories.
- Reasoning with Quantifiers: syntax and semantics of first-order logic with quantifiers; encoding of real-world problems; first-order resolution, superposition, E-matching; implementation of proof search in modern theorem provers; quantifier elimination; quantifier instantiation.
- Interactive Theorem Proving: formal foundations; practical usage of a state-of-the art theorem prover.
- Studijní zdroje a literatura
- Handbook of satisfiability. Edited by Armin Biere. Amsterdam: IOS Press, 2009, xiii, 966. ISBN 9781586039295. info
- Přístupy, postupy a metody používané ve výuce
- Lectures, homework.
- Způsob ověření výstupů z učení a požadavky na ukončení
- Homework, final written exam.
- Vyučovací jazyk
- Angličtina
- Další komentáře
- Studijní materiály
Předmět je vyučován každoročně.
- Statistika zápisu (nejnovější)
- Permalink: https://is.muni.cz/predmet/fi/jaro2026/IA085