UIN3059 Logic and applied computer science 1

Faculty of Philosophy and Science in Opava
Winter 2009
Extent and Intensity
2/2/0. 6 credit(s). Type of Completion: zk (examination).
Teacher(s)
Mgr. Marek Menšík, Ph.D. (lecturer)
Mgr. Marek Menšík, Ph.D. (seminar tutor)
Guaranteed by
Mgr. Marek Menšík, Ph.D.
Institute of Computer Science – Faculty of Philosophy and Science in Opava
Course Enrolment Limitations
The course is also offered to the students of the fields other than those the course is directly associated with.
fields of study / plans the course is directly associated with
Course objectives (in Czech)
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.
Syllabus (in Czech)
  • 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.
Language of instruction
Czech
Further Comments
The course can also be completed outside the examination period.
The course is also listed under the following terms Winter 2010, Winter 2011, Winter 2012, Winter 2013, Winter 2014, Winter 2015, Winter 2016, Winter 2017, Winter 2018, Winter 2019, Winter 2020, Winter 2021, Winter 2022, Winter 2023.
  • Enrolment Statistics (Winter 2009, recent)
  • Permalink: https://is.slu.cz/course/fpf/winter2009/UIN3059