456-0904/01 – Teorie formálních systémů (TFS)

Garantující katedraKatedra informatikyKredity10
Garant předmětuprof. RNDr. Marie Duží, CSc.Garant verze předmětuprof. RNDr. Marie Duží, CSc.
Úroveň studiapostgraduálníPovinnostpovinně volitelný
RočníkSemestrzimní + letní
Jazyk výukyčeština
Rok zavedení1997/1998Rok zrušení2010/2011
Určeno pro fakultyFEIUrčeno pro typy studiadoktorské
Výuku zajišťuje
Os. čís.JménoCvičícíPřednášející
JAN59 prof. RNDr. Petr Jančar, CSc.
Rozsah výuky pro formy studia
Forma studiaZp.zak.Rozsah
prezenční Zápočet a zkouška 3+0
kombinovaná Zápočet a zkouška 3+0

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

Prezenční forma (platnost od: 1960/1961 letní semestr, platnost do: 2012/2013 letní semestr)
Název úlohyTyp úlohyMax. počet bodů
(akt. za podúlohy)
Min. počet bodů
Zápočet a zkouška Zápočet a zkouška 100 (145) 51
        Zkouška Zkouška 100  0
        Zápočet Zápočet 45  0
Rozsah povinné účasti:

Zobrazit historii

Výskyt ve studijních plánech

Akademický rokProgramObor/spec.Spec.ZaměřeníFormaJazyk výuky Konz. stř.RočníkZLTyp povinnosti
2009/2010 (P2646) Informační technologie (1801V002) Informatika a aplikovaná matematika P čeština Ostrava povinně volitelný stu. plán
2009/2010 (P2646) Informační technologie (1801V002) Informatika a aplikovaná matematika K čeština Ostrava povinně volitelný stu. plán
2008/2009 (P2646) Informační technologie (1801V002) Informatika a aplikovaná matematika P čeština Ostrava povinně volitelný stu. plán
2008/2009 (P2646) Informační technologie K čeština Ostrava povinně volitelný stu. plán
2008/2009 (P2646) Informační technologie (1801V002) Informatika a aplikovaná matematika K čeština Ostrava povinně volitelný stu. plán
2007/2008 (P2646) Informační technologie (1801V002) Informatika a aplikovaná matematika P čeština Ostrava povinně volitelný stu. plán
2006/2007 (P2646) Informační technologie (1801V002) Informatika a aplikovaná matematika P čeština Ostrava povinně volitelný stu. plán
2005/2006 (P2646) Informační technologie (1801V002) Informatika a aplikovaná matematika P čeština Ostrava povinně volitelný stu. plán
2004/2005 (P2646) Informační technologie (1801V002) Informatika a aplikovaná matematika P čeština Ostrava povinně volitelný stu. plán
2003/2004 (P2646) Informační technologie (1801V002) Informatika a aplikovaná matematika P čeština Ostrava povinně volitelný stu. plán
2002/2003 (P2612) Elektrotechnika a informatika (1801V002) Informatika a aplikovaná matematika P čeština Ostrava povinně volitelný stu. plán
2001/2002 (P2612) Elektrotechnika a informatika (1801V002) Informatika a aplikovaná matematika P čeština Ostrava povinně volitelný stu. plán

Výskyt ve speciálních blocích

Název blokuAkademický rokForma studiaJazyk výuky RočníkZLTyp blokuVlastník bloku