UINA359 Logic and Applied Computer Science 1

Filozoficko-přírodovědecká fakulta v Opavě
zima 2017
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
In this course, students will be familiar with the base of FOL, especially then with automated methods and theories behind these methods. Students after completion will have a clear idea about the problems of automated derivations. The course is an introductory course to the course Logic and Applied Informatics 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
Vyučovací jazyk
Angličtina
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 2018, zima 2019, zima 2020.