Ukončeno v akademickém roce 2010/2011

Teorie formálních systémů

Typ studia	doktorské
Jazyk výuky	čeština
Kód	456-0904/01
Zkratka	TFS
Název předmětu česky	Teorie formálních systémů
Název předmětu anglicky	Formal Systems
Kreditů	10
Garantující katedra	Katedra informatiky
Garant předmětu	prof. RNDr. Marie Duží, CSc.

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.

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,

zpět na vyhledávání