Detail předmětu

Matematická logika

MLD Ak. rok 2024/2025 letní semestr

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.

Okruhy otázek k SDZ:

  1. Jazyk, formule a sémantika výrokové logiky.
  2. Formální systém výrokové logiky.
  3. Dokazatelnost ve výrokové logice, věta o úplnosti.
  4. Jazyk predikátové logiky, termy a formule.
  5. Sémantika predikátové logiky.
  6. Formální systém predikátové logiky 1. řádu.
  7. Dokazatelnost v predikátové logice, prenexní tvary formulí.
  8. Teorie 1. řádu a jejich modely.  
  9. Věty o úplnosti a o kompaktnosti.
  10. Nerozhodnutelnost teorií 1. řádu, Gödelovy věty o neúplnosti.

 

 

Garant předmětu

Šlapal Josef, prof. RNDr., CSc. (ÚM OAAG)

Koordinátor předmětu

Pavlík Jan, Mgr., Ph.D. (ÚM OAAG)

Jazyk výuky

česky, anglicky

Zakončení

zkouška (kombinovaná)

Rozsah

  • 26 hod. přednášky

Bodové hodnocení

  • 100 bodů závěrečná zkouška

Zajišťuje ústav

ÚM-odbor algebry a diskrétní matematiky (ÚM OAAG)

Cíle předmětu

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

Požadované prerekvizitní znalosti a dovednosti

Předpokládají se znalosti získané v předmětech Diskrétní matematika v bakalářském stupni studia a Matematické struktury v informatice v magisterském stupni studia.

Literatura studijní

  • D.M. Gabbay, C.J. Hogger, J.A. Robinson, Handbook of Logic for Artificial Intellogence and Logic Programming, Oxford Univ. Press 1993
  • A. Sochor, Klasická matematická logika, Karolinum, 2001
  • V. Švejnar, Logika, neúplnost a složitost, Academia, 2002
  • G. Metakides, A. Nerode, Principles of logic and logic programming, Elsevier, 1996
  • Melvin Fitting, First order logic and automated theorem proving, Springer, 1996

Osnova přednášek

  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)

Průběžná kontrola studia

Předmět je hodnocen na základě výsledku závěrečné zkoušky, ke složení zkoušky je třeba získat nejméně 50 z celkového počtu 100 bodů.

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

  • Program DIT, libovolný ročník, povinně volitelný skupina T
  • Program DIT, libovolný ročník, povinně volitelný skupina T
  • Program DIT-EN (anglicky), libovolný ročník, povinně volitelný skupina T
  • Program DIT-EN (anglicky), libovolný ročník, povinně volitelný skupina T
  • Program VTI-DR-4, obor DVI4, libovolný ročník, volitelný
  • Program VTI-DR-4, obor DVI4, libovolný ročník, volitelný
  • Program VTI-DR-4 (anglicky), obor DVI4, libovolný ročník, volitelný
Nahoru