Detail předmětu

Logika

FIT-LOGAk. rok: 2022/2023

V předmětu budou systematicky vyloženy základy výrokové a zejména predikátové logiky. Nejprve budou studenti seznámeni se syntaxí a sémantikou těchto logik, pak budou logiky studovány jako formální teorie s důrazem na problematiku dokazování formulí. Prodiskutovány budou také klasické věty o korektnosti,  úplnosti a kompaktnosti. Po probrání převodu formulí na prenexní tvar budou uvedeny některé vlastnosti a modely teorií 1. řádu. Pozornost bude také věnována nerozhodnutelnosti teorií 1. řádu vyplývající ze známých Gödelových vět o neúplnosti. Závěrem předmětu bude pojednáno o některých dalších významných logikách, které nacházejí uplatnění v informatice.

Jazyk výuky

čeština

Počet kreditů

5

Výsledky učení předmětu

Po absolvování předmětu získají studenti schopnost chápání principů axiomatických matematických teorií i schopnost přesného (formálního) matematického vyjadřování. Naučí se také formálně odvozovat nové formule a dokazovat formule dané. Uvědomí si efektivitu formálního uvažování, ale také jeho hranice.
Studenti se naučí exaktnímu formálnímu myšlení, které jim umožní provádět korektní a efektivní algoritmizaci řešení zadaných problémů. Také získají schopnost ověřovat správnost již vytvořených algoritmizací (verifikace programů).

Prerekvizity

Předpokládají se znalosti získané v předmětu Diskrétní matematika z bakalářského stupně studia.

Způsob a kritéria hodnocení

Půlsemestrální test.

Učební cíle

Cílem předmětu je seznámit studenty se základními metodami uvažování v matematice. Studenti by si měli osvojit obecné principy predikátové logiky a získat tak schopnost přesného matematického uvažování a vyjadřování. Také by se měli naučit pracovat s některými dalšími důležitými formálními teoriemi využívanými v informatice.

Doporučená literatura

D.M. Gabbay, C.J. Hogger, J.A. Robinson, Handbook of Logic for Artificial Intellogence and Logic Programming, Oxford Univ. Press 1993
E. Mendelson, Introduction to Mathematical Logic, Chapman&Hall, 2001
Melvin Fitting, First order logic and automated theorem proving, Springer, 1996
Sally Popkorn, First steps in modal logic, Cambridge Univ. Press, 1994

V. Švejnar, Logika, neúplnost a složitost, Academia, 2002

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

  • Program IT-MGR-2 magisterský navazující

    obor MBI , 0 ročník, letní semestr, volitelný
    obor MBS , 0 ročník, letní semestr, volitelný
    obor MGM , 0 ročník, letní semestr, volitelný
    obor MIN , 0 ročník, letní semestr, volitelný
    obor MIS , 0 ročník, letní semestr, volitelný
    obor MMM , 0 ročník, letní semestr, povinný
    obor MPV , 0 ročník, letní semestr, volitelný

  • Program MITAI magisterský navazující

    specializace NADE , 0 ročník, letní semestr, volitelný
    specializace NBIO , 0 ročník, letní semestr, volitelný
    specializace NCPS , 0 ročník, letní semestr, volitelný
    specializace NEMB , 0 ročník, letní semestr, volitelný
    specializace NGRI , 0 ročník, letní semestr, volitelný
    specializace NHPC , 0 ročník, letní semestr, volitelný
    specializace NIDE , 0 ročník, letní semestr, volitelný
    specializace NISD , 0 ročník, letní semestr, volitelný
    specializace NISY do 2020/21 , 0 ročník, letní semestr, volitelný
    specializace NMAL , 0 ročník, letní semestr, volitelný
    specializace NMAT , 0 ročník, letní semestr, volitelný
    specializace NNET , 0 ročník, letní semestr, volitelný
    specializace NSEC , 0 ročník, letní semestr, volitelný
    specializace NSEN , 0 ročník, letní semestr, volitelný
    specializace NSPE , 0 ročník, letní semestr, volitelný
    specializace NVER , 0 ročník, letní semestr, volitelný
    specializace NVIZ , 0 ročník, letní semestr, volitelný
    specializace NISY , 0 ročník, letní semestr, volitelný

  • Program IT-MGR-2 magisterský navazující

    obor MSK , 1 ročník, letní semestr, povinně volitelný

  • Program MITAI magisterský navazující

    specializace NEMB do 2021/22 , 0 ročník, letní semestr, volitelný

Typ (způsob) výuky

 

Přednáška

26 hod., nepovinná

Vyučující / Lektor

Osnova

  1. Základy teorie množin a kardinální aritmetiky
  2. Jazyk, formule a sémantika výrokové logiky
  3. Formální systém výrokové logiky
  4. Dokazatelnost ve výrokové logice, věta o úplnosti
  5. Jazyk predikátové logiky, termy a formule
  6. Sémantika predikátové logiky
  7. Formální systém predikátové logiky 1. řádu
  8. Dokazatelnost v predikátové logice
  9. Věta o úplnosti a o kompaktnosti, prenexní tvar formulí
  10. Teorie 1. řádu a jejich modely
  11. Nerozhodnutelnost teorií prvního řádu, Gödelovy věty o neúplnosti
  12. Teorie 2. řádu (monadická logika, SkS a WSkS)
  13. Některé další logiky (intuicionistická, modální a temporální logika, Presburgerova aritmetika)

Cvičení odborného základu

26 hod., povinná

Vyučující / Lektor

Osnova

  1. Relační systémy a univerzální algebry
  2. Množiny, kardinální čísla a kardinální aritmetika
  3. Výroky, výrokové spojky, pravdivostní tabulky, tautologie a kontradikce
  4. Nezávislost logických spojek, axiomy výrokové logiky
  5. Věta o dedukci a dokazování formulí výrokové logiky
  6. Termy a formule predikátové logiky
  7. Interpretace, splnitelnost a pravdivost
  8. Axiomy a odvozovací pravidla predikátové logiky
  9. Věta o dedukci a dokazování formulí v predikátové logice
  10. Převody formulí na prenexní tvar
  11. Teorie 1. řádu a jejich modely
  12. Monadické logiky SkS a WSkS
  13. Intuicionistická, modální a temporální logika, Presburgerova aritmetika