Přístupnostní navigace
E-přihláška
Vyhledávání Vyhledat Zavřít
Detail předmětu
FIT-IZLOAk. rok: 2023/2024
Formální výroková a predikátová logika. Syntaxe a sémantika formulí. Normální formy a algebraické úpravy formulí. Formální důkaz jako sekvence aplikací syntaktických pravidel vycházející z axiomů. Prvořádové teorie, modely. Pojmy korektnost, bezespornost, úplnost. Praktické použití SAT a SMT solverů. Souvislost dokazování a počítání, existence limitů dokazování a počítání plynoucí z Gödelových vět.
Jazyk výuky
Počet kreditů
Garant předmětu
Zajišťuje ústav
Vstupní znalosti
Pravidla hodnocení a ukončení předmětu
Hodnocení projektu, který se bude skládat ze dvou příkladů: 1) použití SAT solveru, 2) použití SMT solveru.Projekt hodnocený max. 18 body, písemná zkouška max. 82 body. Pro úspěšné absolvování předmětu je třeba získat alespoň 50 bodů celkem ze 100 a 40 bodů ze zkoušky.
Učební cíle
Prerekvizity a korekvizity
Základní literatura
Doporučení literatura
Elearning
Zařazení předmětu ve studijních plánech
obor BIT , 1 ročník, letní semestr, povinný
Přednáška
Vyučující / Lektor
Osnova
Seminář
Cvičení
Projekt