XD01LOG | Neklasické logiky | Rozsah výuky: | 14+4 | ||
---|---|---|---|---|---|
Přednášející (garant): | Velebil J. | Typ předmětu: | S | Zakončení: | Z,ZK |
Zodpovědná katedra: | 301 | Kreditů: | 4 | Semestr: | L |
Anotace:
Předmět pokrývá moderní partie matematické logiky vhodné pro použití v oblasti formálních metod informatiky: modální a temporální logika jako prostředky pro analýzu korektnosti programů, intuicionismus a teorie typů jako výrazové prostředky formálního dokazování vět. Je uveden i algebraický pohled na matematickou logiku; tj. jsou zavedeny Booleovy, modální, temporální a dynamické algebry jako prostředek matematické logiky. Dále jsou uvedeny základní myšlenky teorie typů.
Osnovy přednášek:
1. | Možnosti klasické výrokové a predikátové logiky. | |
2. | Modální výroková logika. | |
3. | Sémantika možných světů. | |
4. | Věta o korespondenci, modální definovatelnost. | |
5. | Systémy modálních logik. | |
6. | Rozšíření modální logiky: aplikace v CS. | |
7. | Temporální operátory. | |
8. | Sémantika temporální logiky. | |
9. | Logika jako algebra: Booleovy, modální a temporální algebry. | |
10. | Dynamická algebra - sémantika programovacího jazyka. | |
11. | Jiné směry rozšíření klasické logiky: intuicionismus. | |
12. | Logiky vyššího řádu. | |
13. | Základní myšlenky teorie typů. | |
14. | Rezerva. |
Osnovy cvičení:
1. | Možnosti klasické výrokové a predikátové logiky. | |
2. | Modální výroková logika. | |
3. | Sémantika možných světů. | |
4. | Věta o korespondenci, modální definovatelnost. | |
5. | Systémy modálních logik. | |
6. | Rozšíření modální logiky: aplikace v CS. | |
7. | Temporální operátory. | |
8. | Sémantika temporální logiky. | |
9. | Logika jako algebra: Booleovy, modální a temporální algebry. | |
10. | Dynamická algebra - sémantika programovacího jazyka. | |
11. | Jiné směry rozšíření klasické logiky: intuicionismus. | |
12. | Logiky vyššího řádu. | |
13. | Základní myšlenky teorie typů. | |
14. | Rezerva. |
Literatura Č:
1. | S. Popkorn: First Steps in Modal Logic. Cambridge University Press, 1994. | |
2. | A. Galton: Logic for Information Technology. Wiley, Chichester, 1990. |
Literatura A:
1. | Colin Stirling: Modal and Temporal Preperties of Processes. Springer, 2001 | |
2. | Dirk van Dalen: Logic and Structure. Springer, 1980. |
Požadavky:
Podmínkou získání zápočtu je aktivní účast na cvičeních. Upřesnění stanoví cvičící na prvním cvičení.
Předmět je zahrnut do těchto studijních plánů:
|
Stránka vytvořena 25. 2. 2002, semestry: Z/2001-2, Z/2002-3, L/2001-2, L/2002-3, připomínky k informační náplni zasílejte správci studijních plánů | Návrh a realizace: I. Halaška (K336), J. Novák (K336) |