Neklasické logiky

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ů. Je uveden i algebraický pohled na matematickou logiku; tj. jsou zavedeny Booleovy, modální a temporální algebry jako prostředek matematické logiky. Dále budou uvedeny základní myšlenky jiných rozšíření klasické logiky: intuicionismu a teorie typů.

Požadavky:

Podmínkou získání zápočtu je aktivní účast na cvičeních. Hodnocení zkoušky bude dáno výsledkem písemné a ústní části zkoušky konané ve zkouškovém období.

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: Hennessy-Milnerova modální logika.

7. Aplikace modální logiky v CS, sémantika programovacího jazyka.

8. Základní myšlenky mu-kalkulu.

9. Temporální operátory.

10. Sémantika temporální logiky.

11. Symbolický Model Checking.

12. Jiné směry rozšíření klasické logiky.

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: Hennessy-Milnerova modální logika.

7. Aplikace modální logiky v CS, sémantika programovacího jazyka.

8. Základní myšlenky mu-kalkulu.

9. Temporální operátory.

10. Sémantika temporální logiky.

11. Symbolický Model Checking.

12. Jiné směry rozšíření klasické logiky.

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:

Rozsah výuky v kombinované formě studia: 14+4

Typ cvičení: s

Předmět je nabízen i v angličtině.

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

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