I008 Výpočtová logika

Fakulta informatiky
jaro 2000
Rozsah
2/0. 3 kr. (plus ukončení). Doporučované ukončení: zk. Jiná možná ukončení: k, z.
Vyučující
prof. RNDr. Jiří Zlatuška, CSc. (přednášející)
Mgr. Tomáš Dudaško (cvičící)
Garance
prof. RNDr. Mojmír Křetínský, CSc.
Katedra teorie programování – Fakulta informatiky
Kontaktní osoba: prof. RNDr. Jiří Zlatuška, CSc.
Předpoklady
M007 Matematická logika je vítána, ale není nutným předpokladem.
Omezení zápisu do předmětu
Předmět je nabízen i studentům mimo mateřské obory.
Předmět si smí zapsat nejvýše 192 stud.
Momentální stav registrace a zápisu: zapsáno: 0/192, pouze zareg.: 0/192, pouze zareg. s předností (mateřské obory): 0/192
Mateřské obory/plány
Osnova
  • Základy teorie důkazů v predikátové logice a logice prvního řádu: kalkul sekventů a rezoluce.
  • Technické základy: stromy, Königovo lemma, analýza formulí, abstraktní pravdivostní tabulky, klauzulární a duální klauzulární forma.
  • Důkazy ve výrokové logice: systém G, korektnost, úplnost, struktura důkazů, kompaktnost, odstranění řezu; rezoluce, zjemnění rezoluce, Hornovy klauzule, SLD-rezoluce.
  • Důkazy v predikátové logice: substituce, systém G, kompaktnost, Skolemova-Löwenheimova věta, Herbrandova věta; prenexová forma, skolemizace, unifikace, rezoluce a její zjemnění, Hornovy klauzule, SLD-rezoluce.
  • Logické programování: SLD-prohledávání, SLD-rezoluční stromy, sémantika.
Literatura
  • FITTING, Melvin. First order logic and automated theorem proving. 2nd ed. New York: Springer, 1996, xvi, 326. ISBN 0387945938. info
Další komentáře
Předmět je vyučován každoročně.
Výuka probíhá každý týden.
Předmět je zařazen také v obdobích zima 1995, léto 1997, léto 1998, jaro 1999, jaro 2001, jaro 2002.