FPF:UIN3059 Logika a aplik. Informatika 1 - Informace o předmětu
UIN3059 Logika a aplikovaná informatika 1
Filozoficko-přírodovědecká fakulta v Opavězima 2014
- Rozsah
- 2/2/0. 6 kr. Ukončení: zk.
- Vyučující
- Mgr. Marek Menšík, Ph.D. (přednášející)
Mgr. Marek Menšík, Ph.D. (cvičící) - Garance
- Mgr. Marek Menšík, Ph.D.
Ústav informatiky – Filozoficko-přírodovědecká fakulta v Opavě - 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
- Informatika a výpočetní technika (program FPF, N1801 Inf)
- Cíle předmětu
- V tomto kurzu budou studenti obeznámeni se základem prvořádných logik, specielně pak s automatizovanými metodami a teorií na pozadí těchto metod. Studenti po ukončení budou mít jasnou představu o tom, jaké problémy vyvstanou v případě automatizovaného odvozování, případně dokazování. Kurz je směrován jako úvodní kurz ke kurzu Logika a aplikovaná informatika 2.
- Osnova
- Obsah přednášek
1. Logické vyplývání, úsudky, pojem důkazu. Jazyk výrokové logiky, pravdivostní funkce.
2. Sémantika výrokové logiky
3. Automatizované dokazování ve VL (rezoluční metoda)
4. Axiomatický systém Hilbertova typu. Korektnost a úplnost systému
5. Naivní teorie množin, relace, zobrazení
6. Predikátová logika 1. řádu - Úvod.
7. Sémantika (pojem interpretace a modelu, vyplývání).
8. Sémantické metody ověřování správnosti úsudků.
9. Problematika rozhodnutelnosti a rekurzivní vyčíslitelnosti.
10. Věta o dedukci a její vztah k automatizovanému dokazování
11. Rezoluční metoda v PL1: Herbrandova procedura a Robinsonův algoritmus unifikace.
12. Automatizované metody důkazů (obecná rezoluční metoda) a vztah k logickému programování
Obsah cvičení:
Jednotlivá cvičení budou orientována praktickým směrem, kdy si studenti vyzkouší jak formální důkazy, tak se budou zabývat problémy spojené s tématikou budování inferenčních strojů. Současně budou řešit projekt, ve kterém zhodnotí své nabyté znalosti.
- Obsah přednášek
- Další komentáře
- Předmět je dovoleno ukončit i mimo zkouškové období.
- Statistika zápisu (zima 2014, nejnovější)
- Permalink: https://is.slu.cz/predmet/fpf/zima2014/UIN3059