IA085 Satisfiability and Automated Reasoning

Fakulta informatiky
jaro 2024
Rozsah
2/1/1. 4 kr. (plus ukončení). Ukončení: zk.
Vyučující
RNDr. Martin Jonáš, Ph.D. (přednášející)
Bc. 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
St 16:00–17:50 A217
  • Rozvrh seminárních/paralelních skupin:
IA085/01: každé liché pondělí 10:00–11:50 B204, J. Šárník
Omezení zápisu do předmětu
Předmět je otevřen studentům libovolného oboru.
Cíle předmětu
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.
Osnova
  • 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.
Literatura
  • Handbook of satisfiability. Edited by Armin Biere. Amsterdam: IOS Press, 2009, xiii, 966. ISBN 9781586039295. info
Výukové metody
Lectures, homework.
Metody hodnocení
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ě.
Předmět je zařazen také v obdobích jaro 2025.