IA085 Satisfiability and Automated Reasoning

Fakulta informatiky
jaro 2024
Rozsah
2/1/1. 4 kr. (plus ukončení). Ukončení: zk.
Vyučováno prezenčně.
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ě.
  • Statistika zápisu (nejnovější)
  • Permalink: https://is.muni.cz/predmet/fi/jaro2024/IA085