FI:IA038 Typy a důkazy - Informace o předmětu
IA038 Typy a důkazy
Fakulta informatikyjaro 2023
- Rozsah
- 2/0. 2 kr. (plus ukončení). 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
- prof. RNDr. Jiří Zlatuška, CSc.
Katedra teorie programování – Fakulta informatiky
Kontaktní osoba: prof. RNDr. Jiří Zlatuška, CSc.
Dodavatelské pracoviště: Katedra teorie programování – Fakulta informatiky - Rozvrh
- Út 14. 2. až Út 9. 5. Út 12:00–13:50 C511
- 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
- Analýza a zpracování obrazu (program FI, N-VIZ)
- Aplikovaná informatika (program FI, N-AP)
- Bezpečnost informačních technologií (angl.) (program FI, N-IN)
- Bezpečnost informačních technologií (program FI, N-IN)
- Bioinformatika a systémová biologie (program FI, N-UIZD)
- Bioinformatika (program FI, N-AP)
- Computer Games Development (program FI, N-VIZ_A)
- Computer Graphics and Visualisation (program FI, N-VIZ_A)
- Computer Networks and Communications (program FI, N-PSKB_A)
- Cybersecurity Management (program FI, N-RSSS_A)
- Diskrétní algoritmy a modely (program FI, N-TEI)
- Formální analýza počítačových systémů (program FI, N-TEI)
- Grafický design (program FI, N-VIZ)
- Graphic Design (program FI, N-VIZ_A)
- Hardware Systems (program FI, N-PSKB_A)
- Hardwarové systémy (program FI, N-PSKB)
- Image Processing and Analysis (program FI, N-VIZ_A)
- Informační bezpečnost (program FI, N-PSKB)
- Informační systémy (program FI, N-IN)
- Information Security (program FI, N-PSKB_A)
- Kvantové a jiné neklasické výpočetní modely (program FI, N-TEI)
- Paralelní a distribuované systémy (program FI, N-IN)
- Počítačová grafika a vizualizace (program FI, N-VIZ)
- Počítačová grafika (program FI, N-IN)
- Počítačové sítě a komunikace (program FI, N-IN)
- Počítačové sítě a komunikace (program FI, N-PSKB)
- Počítačové systémy (program FI, N-IN)
- Principy programovacích jazyků (program FI, N-TEI)
- Programovatelné technické struktury (angl.) (program FI, N-IN)
- Programovatelné technické struktury (program FI, N-IN)
- Řízení kyberbezpečnosti (program FI, N-RSSS)
- Řízení vývoje služeb (program FI, N-RSSS)
- Řízení vývoje softwarových systémů (program FI, N-RSSS)
- Services Development Management (program FI, N-RSSS_A)
- Služby - výzkum, řízení a inovace (angl.) (program FI, N-AP)
- Služby - výzkum, řízení a inovace (program FI, N-AP)
- Sociální informatika (program FI, B-AP)
- Software Systems Development Management (program FI, N-RSSS_A)
- Software Systems (program FI, N-PSKB_A)
- Softwarové systémy (program FI, N-PSKB)
- Strojové učení a umělá inteligence (program FI, N-UIZD)
- Teoretická informatika (program FI, N-IN)
- Učitelství výpočetní techniky pro střední školy (program FI, N-SS) (2)
- Umělá inteligence a zpracování přirozeného jazyka (program FI, N-IN)
- Vývoj počítačových her (program FI, N-VIZ)
- Zpracování a analýza rozsáhlých dat (program FI, N-UIZD)
- Zpracování obrazu (program FI, N-AP)
- Zpracování přirozeného jazyka (program FI, N-UIZD)
- Cíle předmětu
- Přednáška pojednává seznamuje s vazbou teorie důkazů na typovaný lambda-kalkul resp. obecně se souvislostí teorie důkazů a mechanismů popisujících kroky výpočetních procesů jako zjednodušování důkazů v různých formalismech. Seznamuje s aparátem, který je podstatný pro práci v řadě oblastí teoretické informatiky.
- 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.
- Literatura
- Další komentáře
- Studijní materiály
Předmět je vyučován jednou za dva roky.
- Statistika zápisu (jaro 2023, nejnovější)
- Permalink: https://is.muni.cz/predmet/fi/jaro2023/IA038