IA085 Satisfiability and Automated Reasoning

Fakulta informatiky
jaro 2027
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
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
Předmět je vyučován každoročně.
Výuka probíhá každý týden.
Předmět je zařazen také v obdobích jaro 2024, jaro 2025, jaro 2026.