Detail předmětu
Logika
LOG Ak. rok 2021/2022 letní semestr 5 kreditů
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.
Garant předmětu
Jazyk výuky
Zakončení
Rozsah
- 26 hod. přednášky
 - 26 hod. cvičení
 
Bodové hodnocení
- 60 bodů závěrečná zkouška
 - 20 bodů půlsemestrální test
 - 20 bodů numerická cvičení
 
Zajišťuje ústav
Přednášející
Cvičící
Získané dovednosti, znalosti a kompetence z 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ů).
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.
Požadované prerekvizitní znalosti a dovednosti
Předpokládají se znalosti získané v předmětu Diskrétní matematika z bakalářského stupně 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
 - E. Mendelson, Introduction to Mathematical Logic, Chapman&Hall, 2001
 - A. Nerode, R.A. Shore, Logic for Applications, Springer-Verlag 1993
 - D.M. Gabbay, C.J. Hogger, J.A. Robinson, Handbook of Logic for Artificial Intelligence 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
 - Sally Popkorn, First steps in modal logic, Cambridge Univ. Press, 1994
 
Osnova přednášek
- 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)
 
Osnova numerických cvičení
- Relační systémy a univerzální algebry
 - Množiny, kardinální čísla a kardinální aritmetika
 - Výroky, výrokové spojky, pravdivostní tabulky, tautologie a kontradikce
 - Nezávislost logických spojek, axiomy výrokové logiky
 - Věta o dedukci a dokazování formulí výrokové logiky
 - Termy a formule predikátové logiky
 - Interpretace, splnitelnost a pravdivost
 - Axiomy a odvozovací pravidla predikátové logiky
 - Věta o dedukci a dokazování formulí v predikátové logice
 - Převody formulí na prenexní tvar
 - Teorie 1. řádu a jejich modely
 - Monadické logiky SkS a WSkS
 - Intuicionistická, modální a temporální logika, Presburgerova aritmetika
 
Průběžná kontrola studia
Půlsemestrální test.
Podmínky zápočtu
Pravidelná docházka na cvičení a úspěšné složení obou kontrolních testů
Zařazení předmětu ve studijních plánech
- Program IT-MGR-2, obor MBI, MBS, MGM, MIN, MIS, MPV, libovolný ročník, volitelný
 - Program IT-MGR-2, obor MMM, libovolný ročník, povinný
 - Program IT-MGR-2, obor MSK, 1. ročník, povinně volitelný skupina M
 - Program MITAI, obor NADE, NBIO, NCPS, NEMB, NGRI, NHPC, NIDE, NISD, NISY, NISY do 2020/21, NMAL, NMAT, NNET, NSEC, NSEN, NSPE, NVER, NVIZ, libovolný ročník, volitelný