Detail předmětu
Matematická logika
FIT-MLDAk. rok: 2024/2025
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:
- Jazyk, formule a sémantika výrokové logiky.
- Formální systém výrokové logiky.
- Dokazatelnost ve výrokové logice, věta o úplnosti.
- Jazyk predikátové logiky, termy a formule.
- Sémantika predikátové logiky.
- Formální systém predikátové logiky 1. řádu.
- Dokazatelnost v predikátové logice, prenexní tvary formulí.
- Teorie 1. řádu a jejich modely.
- Věty o úplnosti a o kompaktnosti.
- Nerozhodnutelnost teorií 1. řádu, Gödelovy věty o neúplnosti.
Jazyk výuky
Garant předmětu
Zajišťuje ústav
Vstupní znalosti
Pravidla hodnocení a ukončení předmětu
Učební cíle
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ů).
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
G. Metakides, A. Nerode, Principles of logic and logic programming, Elsevier, 1996
Melvin Fitting, First order logic and automated theorem proving, Springer, 1996
V. Švejnar, Logika, neúplnost a složitost, Academia, 2002
Zařazení předmětu ve studijních plánech
- Program DIT doktorský 0 ročník, letní semestr, povinně volitelný
- Program DIT doktorský 0 ročník, letní semestr, povinně volitelný
- Program DIT-EN doktorský 0 ročník, letní semestr, povinně volitelný
- Program DIT-EN doktorský 0 ročník, letní semestr, povinně volitelný
- Program VTI-DR-4 doktorský
obor DVI4 , 0 ročník, letní semestr, volitelný
- Program VTI-DR-4 doktorský
obor DVI4 , 0 ročník, letní semestr, volitelný
- Program VTI-DR-4 doktorský
obor DVI4 , 0 ročník, letní semestr, volitelný
Typ (způsob) výuky
Přednáška
Vyučující / Lektor
Osnova
- Základy teorie množin a kardinální aritmetiky
- Jazyk, formule a sémantika výrokové logiky
- Formální systém výrokové logiky
- Dokazatelnost ve výrokové logice, věta o úplnosti
- Jazyk predikátové logiky, termy a formule
- Sémantika predikátové logiky
- Formální systém predikátové logiky 1. řádu
- Dokazatelnost v predikátové logice
- Věta o úplnosti a o kompaktnosti, prenexní tvar formulí
- Teorie 1. řádu a jejich modely
- Nerozhodnutelnost teorií prvního řádu, Gödelovy věty o neúplnosti
- Teorie 2. řádu (monadická logika, SkS a WSkS)
- Některé další logiky (intuicionistická, modální a temporální logika, Presburgerova aritmetika)