Detail předmětu
Logika
LOG Ak. rok 2009/2010 zimní 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 kompaktnosti a úplnosti. 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 včetně logik 2. řádu, které nacházejí uplatnění v informatice.
Garant předmětu
Jazyk výuky
Zakončení
Rozsah
- 39 hod. přednášky
- 13 hod. cvičení
Zajišťuje ústav
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 formálních (axiomatických) teorií 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 nejdůležitější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í
- 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 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
- Sally Popkorn, First steps in modal logic, Cambridge Univ. Press, 1994
- A. Sochor, Klasická matematická logika, Karolinum, 2001
- V. Švejnar, Logika, neúplnost a složitost, Academia, 2002
Literatura referenční
- 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
Hodnocení studia je založeno na bodovacím systému. Pro úspěšné absolvování předmětu je nutno dosáhnout 50 bodů.
Kontrolovaná výuka
Půlsemestrální test.
Zařazení předmětu ve studijních plánech