UIN3059 Logika a aplikovaná informatika 1

Filozoficko-přírodovědecká fakulta v Opavě
zima 2012
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
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.
Další komentáře
Předmět je dovoleno ukončit i mimo zkouškové období.
Předmět je zařazen také v obdobích zima 2009, zima 2010, zima 2011, zima 2013, zima 2014, zima 2015, zima 2016, zima 2017, zima 2018, zima 2019, zima 2020, zima 2021, zima 2022, zima 2023.