Přehled studia | Přehled oborů | Všechny skupiny předmětů | Všechny předměty | Seznam rolí | Vysvětlivky               Návod
01LP Logika programů Rozsah výuky:2+2
Přednášející (garant):  Typ předmětu:S Zakončení:Z,ZK
Zodpovědná katedra:301 Kreditů:4 Semestr:L

Anotace:
Akční struktury, Milnerův jazyk CCS. Hennessy-Milnerova modální logika. Aplikace na jazyk WHILE - částečná korektnost programů. Minimální modální logika, úplnost a rozhodnutelnost. Věta o korespondenci a modální definovatelnost. Kleeneho věta o pevném bodě. Rekursivní rovnice v posetu. Modální m-kalkulus a m-rovnice, l- kalkulus a teorie typů. Redukce v l-kalkulu.

Osnovy přednášek:
1. Množiny, relace, uspořádání
2. Akční struktury, Milnerův jazyk CCS
3. Hennessy-Milnerova modální logika
4. Aplikace na jazyk WHILE - částečná korektnost programů
5. Minimální modální logika
6. Úplnost a rozhodnutelnost minimální modální logiky
7. Věta o korespondenci a modální definovatelnost
8. Kleeneho věta o pevném bodě. Rekursivní rovnice v posetu
9. Modální ?-kalkulus
10. Modální ?-rovnice
11. ?-kalkulus a teorie typů
12. Redukce v ?-kalkulu
13. Návrh sémantiky programovacího jazyka
14. Rezerva

Osnovy cvičení:
1. Množiny, relace, uspořádání
2. Akční struktury, Milnerův jazyk CCS
3. Hennessy-Milnerova modální logika
4. Aplikace na jazyk WHILE - částečná korektnost programů
5. Minimální modální logika
6. Úplnost a rozhodnutelnost minimální modální logiky
7. Věta o korespondenci a modální definovatelnost
8. Kleeneho věta o pevném bodě. Rekursivní rovnice v posetu
9. Modální ?-kalkulus
10. Modální ?-rovnice
11. ?-kalkulus a teorie typů
12. Redukce v ?-kalkulu
13. Návrh sémantiky programovacího jazyka
14. Rezerva

Literatura Č:

Literatura A:

Požadavky:

Rozsah výuky v kombinované formě studia: 14+4
Typ cvičení: s

Předmět je zahrnut do těchto studijních plánů:
Plán Obor Role Dop. semestr
*BIO Biomedicínské inženýrství F >7


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)