456-0349/01 – Matematická logika (ML)
| Garantující katedra | Katedra informatiky | Kredity | 8 |
| Garant předmětu | prof. RNDr. Marie Duží, CSc. | Garant verze předmětu | prof. RNDr. Marie Duží, CSc. |
| Úroveň studia | pregraduální nebo graduální | Povinnost | povinně volitelný |
| Ročník | 1 | Semestr | zimní |
| | Jazyk výuky | čeština |
| Rok zavedení | 2006/2007 | Rok zrušení | 2009/2010 |
| Určeno pro fakulty | FEI | Určeno pro typy studia | navazující magisterské |
Cíle předmětu vyjádřené dosaženými dovednostmi a kompetencemi
Cílem předmětu je seznámení se základními principy logických kalkulů a axiomatických teorií, a jejich rozvinutí v oblasti algebry, zejména teorie svazů. Kurs je zaměřen na praktické aplikace v různých oblastech teoretické a aplikované informatiky při zachování exaktnosti jak při formulaci problému, tak při jeho řešení.
Vyučovací metody
Přednášky
Individuální konzultace
Cvičení (v učebně)
Anotace
Cílem předmětu je seznámit studenty s pojmovým aparátem a metodami výrokové logiky, predikátové logiky 1. řádu a teorií formálních systémů. Tento aparát a tyto metody jsou běžně používány v různých oblastech informatiky (precizace a formalizace intuitivních poznatků a teorií, automatizace dokazování a vyvozování, umělá inteligence ...) a mnoha jiných exaktních disciplínách.
Povinná literatura:
M.Duží: Matematická logika. Učební texty VŠB Ostrava.
http://www.cs.vsb.cz/duzi/Mat-logika.html
Z. Manna: Matematická teorie programů. McGraw-Hill, 1974, SNTL Praha 1981.
Doporučená literatura:
Švejdar, V.: Logika (neúplnost, složitost, nutnost). Academia, Praha 2002.
Sochor, A.: Klasická matematická logika. Karolinum Praha, 2001.
Brown, J.R.: Philosophy of Mathematics. Routledge, 1999.
Thayse, A.: From Standard Logic to Logic Programming, John Wiley & Sons, 1988
Nerode, Anil - Shore, Richard A. Logic for applications. New York : Springer-Verlag, 1993. Texts and Monographs in Computer Science.
Richards, T.: Clausal Form Logic. An Introduction to the Logic of Computer Reasoning. Adison-Wesley, 1989.
Bibel, W.: Deduction (Automated Logic). Academia Press, 1993.
Fitting, Melvin. First order logic and automated theorem proving [1996]. 2nd ed. New York : Springer, 1996. Graduate texts in computer science.
Forma způsobu ověření studijních výsledků a další požadavky na studenta
Podmínky udělení zápočtu:
V průběhu semestru budou tři písemné testy. Z každého může student získat max. 10 bodů.
Maximum bodů, které lze získat na zápočet = 30 bodů.
Minimální počet bodů pro získání zápočtu = 15.
E-learning
Další požadavky na studenta
Prerekvizity
Předmět nemá žádné prerekvizity.
Korekvizity
Předmět nemá žádné korekvizity.
Osnova předmětu
Přednášky:
Naivní teorie množin: množinové operace a jejich definice prostředky predikátové logiky 1. řádu (PL1). Kartézský součin, relace, zobrazení.
Sémantické metody predikátové logiky 1. řádu (PL1)
Úvod do formálních (důkazových) kalkulů
Rezoluční metoda ve výrokové logice
Obecná rezoluční metoda v PL1
Přirozená dedukce ve výrokové logice
Přirozená dedukce v PL1
Korektnost a úplnost kalkulu
Presentace řešení samostatných projektů - příkladů.
Teorie relací, typy relací, teorie ekvivalence a uspořádání.
Algebraické teorie, grupy, okruhy, tělesa.
Teorie svazů, konceptuální svazy
Formalizované teorie aritmetiky, Gödelovy výsledky (věty o neúplnosti)
Formální kalkuly Hilbertova typu pro výrokovou logiku a predikátovou logiku
Cvičení:
Deduktivně platné úsudky
Naivní teorie množin
Výroková logika, jazyk a sémantika
Výroková logika, rezoluční metoda dokazování
Predikátová logika, jazyk a sémantika, modely
Relace, funkce, spočetnost a nespočetnost množin
Sémantická tabla
Aristotelova logika
Obecná rezoluční metoda v PL1
Důkazové kalkuly: přirozená dedukce a Hilbertův kalkul
Teorie relací, funkcí, algebraické teorie
Projekty:
Řešení zadaného problému metodou přirozené dedukce a rezoluční metodou.
Podmínky absolvování předmětu
Výskyt ve studijních plánech
Výskyt ve speciálních blocích
Hodnocení Výuky