Detail předmětu

Základy logiky pro informatiky

IZLO Ak. rok 2022/2023 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
  • 12 hod. cvičení
  • 2 hod. projekty

Bodové hodnocení

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

Zajišťuje ústav

Přednášející

Cvičící

Získané dovednosti, znalosti a kompetence z předmětu

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ů.

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.

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 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 numerických cvičení

  1. SAT a SMT solving

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.

Kontrolovaná výuka

Projekt hodnocený max. 20 body, písemná zkouška max. 80 body. Pro úspěšné absolvování předmětu je třeba získat alespoň 50 bodů celkem ze 100 a polovinu bodů ze zkoušky (t.j. 40 bodů z 80).

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

Nahoru