FI:IA085 SAT and Automated Reasoning - Informace o předmětu

IA085 Satisfiability and Automated Reasoning

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í)
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

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

Předmět je vyučován každoročně.
Výuka probíhá každý týden.

• Statistika zápisu (nejnovější)
  
• Permalink: https://is.muni.cz/predmet/fi/jaro2025/IA085