I008 Výpočtová logika

Fakulta informatiky
jaro 2001
Rozsah
2/0. 3 kr. (plus ukončení). Doporučované ukončení: zk. Jiná možná ukončení: k, z.
Vyučující
doc. RNDr. Lubomír Popelínský, Ph.D. (přednášející)
Mgr. Miloslav Nepil, Ph.D. (cvičící)
Garance
prof. RNDr. Mojmír Křetínský, CSc.
Katedra teorie programování – Fakulta informatiky
Kontaktní osoba: doc. RNDr. Lubomír Popelínský, Ph.D.
Rozvrh
Čt 17:00–18:50 D1 a každé liché pondělí 13:00–14:50 D2 a každé sudé pondělí 13:00–14:50 D2
  • Rozvrh seminárních/paralelních skupin:
I008/1: Rozvrh nebyl do ISu vložen.
I008/2: Rozvrh nebyl do ISu vložen.
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 253 stud.
Momentální stav registrace a zápisu: zapsáno: 0/253, pouze zareg.: 0/253, pouze zareg. s předností (mateřské obory): 0/253
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ě.
Předmět je zařazen také v obdobích zima 1995, léto 1997, léto 1998, jaro 1999, jaro 2000, jaro 2002.