Neklasické logiky (dálk.)

Přednášející:

Cvičící:

Předmět zajišťuje:

katedra matematiky

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

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í.

Osnova 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.

Osnova 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.

Cíle studia:

Studijní materiály:

1. S. Popkorn: First Steps in Modal Logic. Cambridge University Press, 1994.

2. A. Galton: Logic for Information Technology. Wiley, Chichester, 1990.

Poznámka:

Další informace:

Pro tento předmět se rozvrh nepřipravuje

Předmět je součástí následujících studijních plánů:

• Výpočetní technika - softwarové inženýrství- strukturované studium (povinně volitelný předmět)
• Výpočetní technika - systémové programování- strukturované studium (povinně volitelný předmět)
• Výpočetní technika - počítačová grafika- strukturované studium (povinně volitelný předmět)
• Výpočetní technika - počítačové sítě a internet- strukturované studium (povinně volitelný předmět)
• Výpočetní technika - projektování číslicových systémů- strukturované studium (povinně volitelný předmět)