UIN3059 Logika a aplikovaná informatika 1

Filozoficko-přírodovědecká fakulta v Opavě
zima 2021
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ě
Rozvrh seminárních/paralelních skupin
UIN3059/A: Rozvrh nebyl do ISu vložen. M. Menšík
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.
Literatura
    doporučená literatura
  • Marie Duží. Matematická logika. Skripta VŠB-TU v Ostravě. URL info
  • ing M. Copi, Carl Cohen, Kenneth McMahon. Introduction to Logic. Routledge, 2013. ISBN 9780205820375. info
  • Duží Marie. Procedural semantics for hyperintensional logic : foundations and applications of transparent intensional logic. Dordrecht, 2010. ISBN 978-90-481-8811-6. info
  • ŠTĚPÁN, J. Formální logika. Olomouc, 1995. info
Výukové metody
Přednáška s aktivizací
Přednáška s analýzou videozáznamu
Metody hodnocení
Zkouška
Informace učitele
Teoretické a praktické zvládnutí témat předmětu, podmínky budou upřesněny na začátku výuky.
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 2012, zima 2013, zima 2014, zima 2015, zima 2016, zima 2017, zima 2018, zima 2019, zima 2020, zima 2022, zima 2023.