Detail předmětu

Základy logiky pro informatiky

IZLO Ak. rok 2023/2024 letní semestr 2 kredity

Aktuální akademický rok

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.

Garant předmětu

Koordinátor předmětu

Jazyk výuky

česky

Zakončení

zkouška (písemná)

Rozsah

  • 10 hod. přednášky
  • 2 hod. seminář
  • 10 hod. cvičení
  • 2 hod. projekty

Bodové hodnocení

  • 82 bodů závěrečná zkouška (písemná část)
  • 18 bodů projekty

Zajišťuje ústav

Přednášející

Cvičící

Cíle předmětu

Seznámení s nejzákladnějšími pojmy, koncepty a výsledky klasické matematické logiky (související se syntaxí, sémantikou a dokazováním ve výrokové a predikátové logice); nacvičení formálního vyjadřování pomocí aparátu matematické logiky; uvedení do souvislostí počítání, formálního logického usuzování a jejich limitů; seznámení s praktickými technologiemi automatického logického usuzování - SAT a SMT solving.
Orientace v pojmech matematické logiky jako term, formule, axiom, důkaz, syntaxe, sémantika, splnitelnost, platnost, korektnost, spornost, úplnost, axiom, důkaz. Schopnost práce s jazykem výrokové a predikátové logiky: důkladné porozumění významu a použití symbolům výrokové a predikátové logiky, spojek, kvantifikátorů, logických proměnných. Schopnost psát a číst texty s prvky formální notace. Zlepšení celkové schopnosti formálního a přesného vyjadřování a myšlení. Základní znalost nejzásadnějších výsledků v matematické logice, Gödelových vět, a jejich významu pro informatiku. Povědomí o praktickém užití SAT a SMT solverů.

Proč je předmět vyučován

Základní pojmy a koncepty matematické logiky stály na samém počátku informatiky a prostupují ji na každém kroku. Stojí v pozadí logických obvodů, procesorů, a téměř každého formálního systému nebo jazyka, včetně těch programovacích, specifikačních, modelovacích. Seznámit se s nimi důkladně v jejich původní formě pomůže orientovat se v odvozených konceptech moderní informatiky.

Studium matematické logiky, vědy o formálním vyjadřování a usuzování, je také unikátní příležitostí důkladně procvičit přesné a srozumitelné vyjadřování a usuzování, které je kritickou dovedností v každé oblasti IT. Informatik neustále potřebuje vstřebávat, vytvářet a komunikovat komplikované algoritmy, modely, systémy, specifikace…

SAT a SMT solving je příkladem praktického použití vyučované teorie. Je univerzální technologií použitelnou v plánování, řešení aritmetických problémů, grafových problémů, v analýze programů, testování a verifikaci, a dalších odvětvích.

Nakonec, základní fakta o souvislosti počítání, formálního usuzování a matematického dokazování, a o existenci jejich limitů plynoucích z Gödelových vět, patří mezi nejzásadnější teoretickými poznatky informatiky vůbec.

Doporučené prerekvizity

Požadované prerekvizitní znalosti a dovednosti

Základy diskrétní matematiky a matematické notace, množiny, relace, zobrazení.

Literatura studijní

  • Herbert B. Enderton. A Mathematical Introduction to Logic. Academic Press, 2001. ISBN 978-0122384523

Literatura referenční

  • Herbert B. Enderton. A Mathematical Introduction to Logic. Academic Press, 2001. ISBN 978-0122384523
  • Michael Huth and Mark Ryan. Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press, 2004. ISBN 978-0521543101
  • Peter Smith. An Introduction to Formal Logic. ISBN 978-1916906327 https://www.logicmatters.net/ifl/
  • Peter Smith. Gödel Without (Too Many) Tears. ISBN 979-8673862131 https://www.logicmatters.net/igt/
  • Doxiadis A, Papadimitriou C. LOGICOMIX: an epic search for truth. Bloomsbury Publishing USA; 2015 Jul 28. ISBN 978-1596914520

Osnova přednášek

  1. Úvod, syntaxe a sémantika výrokové logiky, splnitelnost, platnost, tabulky, konjunktivní a disjunktivní normální forma, algebraické úpravy formulí, úplné systémy spojek.
  2. Syntaxe a sémantika predikátové logiky.
  3. Normální formy a algebraické úpravy predikátových formulí. Teorie v predikátové logice.
  4. Dokazování. Důkaz z axiomů pomocí odvozovacích pravidel. Vztah syntaxe a sémantiky. Efektivní, korektní, úplný dokazovací systém.
  5. Bezespornost a úplnost prvořádových teorií. Vztah počítání a dokazování, mechanizovatelnost matematiky a teorií PL, Gödelovy věty o neúplnosti.

Osnova seminářů

  1. SAT a SMT solving.

Osnova cvičení

  1. Výroková logika: formalizace tvrzení, splňování formulí, tabulky, převody do CNF a DNF.
  2. Predikátová logika: kvantifikátory a proměnné. Formalizace a porozumění formulím 1.
  3. Predikátová logika: interpretace jazyka, model formule. Formalizace a porozumění formulím 2.
  4. Algebraické úpravy a převody do normálních forem.
  5. Dokazování.

Osnova ostatní - projekty, práce

  1. Použití SAT solverů
  2. Použití SMT solverů

Průběžná kontrola studia

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.

Zařazení předmětu ve studijních plánech

Nahoru