456-0904/01 – Teorie formálních systémů (TFS)
| Garantující katedra | Katedra informatiky | Kredity | 10 |
| Garant předmětu | prof. RNDr. Marie Duží, CSc. | Garant verze předmětu | prof. RNDr. Marie Duží, CSc. |
| Úroveň studia | postgraduální | Povinnost | povinně volitelný |
| Ročník | | Semestr | zimní + letní |
| | Jazyk výuky | čeština |
| Rok zavedení | 1997/1998 | Rok zrušení | 2010/2011 |
| Určeno pro fakulty | FEI | Určeno pro typy studia | doktorské |
Cíle předmětu vyjádřené dosaženými dovednostmi a kompetencemi
Cílem je seznámit studenty s pojmovým aparátem a metodami logiky 1.řádu a s teorií obecných formálních systémů, které logiku 1.řádu obsahují jako svou nedílnou část. Tento aparát a tyto metody jsou běžně používány v různých oblastech informatiky (formalní specifikace informačních systémů, automatizace dokazování a vyvozování, umělá inteligence ...) a mnoha dalších oborech.
Vyučovací metody
Anotace
Předmět rekapituluje a rozvíjí obsah předmětu Matematická logika přednášený v magisterském studiu. Důraz se přenáší z výkladu pouhé matematické logiky na obecné deduktivní formální systémy, které obsahují formální logiku jako svou nedílnou část.
Povinná literatura:
A.Thayse et al.: From standard logic to logic programming /Introducing a logic based approach to arificial intelligence/. John Wiley and Sons, 1989
Duží, M.: Matematická logika. Učební texty v elektronické podobě, http://www.cs.vsb.cz/duzi/matlogika.html VŠB -TU Ostrava, 2004.
Metakides, G., Nerode, A.: Principles of Logic and Logic Programming. Elsevier 1996.
Kolář, J.-Štěpánková¨, O -Chytil, M.: Logika, algebra, grafy. Praha, SNTL 1989.
Lukasová, A.: Logické základy umělé inteligence, skripta PF Ostravské univerzity, 1999
Doporučená literatura:
T Richards: Clausal form logic /An Introduction to the logic of computer reasoning/ Addison-Wesley, 1989
W.Bibel: Deduction /Automated Logic/. Academic Press, San Diego, 1993
Nerode, Anil - Shore, Richard A. Logic for applications. New York : Springer-Verlag, 1993. Texts and Monographs in Computer Science.
Fitting, Melvin. First order logic and automated theorem proving [1996]. 2nd ed. New York : Springer, Graduate texts in computer science.
F.Kroeger: Temporal Logic of Programs. Springer-Verlag,
Forma způsobu ověření studijních výsledků a další požadavky na studenta
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:
Hierarchie logik. Logika 1.řádu. Pojem formule a definice jazyka logiky 1.řádu.
Sémantický výklad logiky 1.řádu. Relace definované na množině formulí /sémantická ekvivalence a vyplývání/.
Kanonické tvary formulí: prenexní tvar, skolemizace.
Gentzenovské systémy přirozené dedukce logiky 1.řádu.
Axiomatické systémy logiky 1.řádu.
Věty o dedukci, korektnosti a sémantické úplnosti.
Automatické dokazování: rezoluce, unifikace, Robinsonův princip, logické programy.
Reprezentace znalostí a logické vyvozování.
Modální logiky.
Temporální logika.
Metamatematika jako teorie formálních systémů. Definice pojmů uvnitř formálních systémů.
Vlastnosti formálních systémů: bezespornost, úplnost, rozhodnutelnost, kategoričnost, nezávislost axiómů. Formalizovaná teorie přirozených čísel a množin.
Omezené možnosti formalizace. Gödelovy věty.
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
Předmět neobsahuje žádné hodnocení.