UIN3059 Logika a aplikovaná informatika 1

Filozoficko-přírodovědecká fakulta v Opavě
zima 2023
Rozsah
2/2/0. 6 kr. Ukončení: zk.
Vyučující
RNDr. Radka Poláková, Ph.D. (přednášející)
Mgr. Jan Schreier (přednášející)
Mgr. Jan Schreier (cvičící)
Garance
RNDr. Radka Poláková, Ph.D.
Ústav informatiky – Filozoficko-přírodovědecká fakulta v Opavě
Rozvrh
Po 16:25–18:00 LEI
  • Rozvrh seminárních/paralelních skupin:
UIN3059/A: Po 18:05–19:40 LEI, J. Schreier
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 2021, zima 2022.
  • Statistika zápisu (nejnovější)
  • Permalink: https://is.slu.cz/predmet/fpf/zima2023/UIN3059