FPF:UIN3059 Logic and Applied Computer Sci - Course Information
UIN3059 Logic and Applied Computer Science 1
Faculty of Philosophy and Science in OpavaWinter 2010
- 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
- Computer Science and Technology (programme FPF, M1801 Inf)
- Computer Science and Technology (programme FPF, N1801 Inf)
- 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.
- Obsah přednášek
- Language of instruction
- Czech
- Further Comments
- The course can also be completed outside the examination period.
- Enrolment Statistics (Winter 2010, recent)
- Permalink: https://is.slu.cz/course/fpf/winter2010/UIN3059