FI:I038 Typy a důkazy - Informace o předmětu

I038 Typy a důkazy

Fakulta informatiky
zima 1997

Rozsah

2/0. 3 kr. Doporučované ukončení: zk. Jiná možná ukončení: k, z.

Vyučující

prof. RNDr. Jiří Zlatuška, CSc. (přednášející)

Garance

Kontaktní osoba: prof. RNDr. Jiří Zlatuška, CSc.

Omezení zápisu do předmětu

Předmět je nabízen i studentům mimo mateřské obory.

Mateřské obory/plány

Osnova

Význam a denotace v logice, Tarski a Heyting.
Přirozená dedukce: kalkul, pravidla, výpočetní interpretace.
Curryho-Howardův izomorfismus: lambda-kalkul, operační a denotační interpretace, konverze, izomorfismus.
Věta o normalizaci: Churchova--Rosserova vlastnost, věta o slabé normalizaci, věta o silné normalizaci.
Kalkul sekventů: strukturální pravidla, intuicionistická varianta, identity, logická pravidla, vlastnosti systému bez řezu, překlad mezi kalkulem sekventů a přirozenou dedukcí.
Věta o silné normalizaci: reducibilita a její vlastnosti.
Gödelův systém T, kalkul, normalizace, výrazové schopnosti.
Koherentní prostory, stabilní funkce, paralelní disjunkce, součinové a funkční prostory, denotační sémantika systému T.
Součty v přirozené dedukci: problémy, standardní konverze, komutující konverze, funkční kalkul.
Systém F: kalkul, jednoduché typy, volné struktury, induktivní typy, Curryho--Howardův izomorfismus, silná normalizace.
Koherentní sémantika součtů; věta o odstranění řezu; reprezentace.