Studentsky logicky seminar



Vyucujici: Jan Krajicek

Kody predmetu:
zimni semestr NALG050: Studentsky logicky seminar I.
letni semestr NALG051: Studentsky logicky seminar II.
(seminar lze zapsat opakovane)

Studentsky logicky seminar je minen pro studenty se zajmem o matematickou logiku. Nevyzaduje "vetsi nez male" znalosti matematicke logiky, napr. na urovni uvodniho kursu (jeho absolvovani ale neni podminkou). Seminar bezi od letniho semestru 06/07. Studenti jsou vitani i na pokrocilem Logickem seminari.

V kazdem semestru probirame jine tema - k porozumeni latky neni potreba ucast na seminari v predchozich semestrech. Temata jsou volena s ohledem na zajmy a znalosti ucastniku a vetsinou maji primy ci neprimy vztah k oblasti

"Logika & Slozitost".

Obcas mame prednasky hostu na ruzna pristupna temata relevantni k hlavni probirane latce.

Drivejsi program (podrobnosti):

  • Letni semestr 06/07: Teorie konecnych modelu

  • Zimni semestr 07/08: Studium clanku
    Dana Scott, A proof of the independence of the continuum hypothesis, Mathematical Systems Theory, 1, (1967), str.89-111.

  • Letni semestr 07/08: Omezena aritmetika
    Paralelne s timto tematem oragizoval student p.Jan Pich dalsi studium literatury o konecne teorii modelu, zejmena skripta M.Otta - viz informace o letni semestru 06/07 vyse (ucast na tomto drivejsim seminari neni podminkou).

  • Zimni semestr 08/09: Booleovska slozitost

    Program letniho semestru 08/09: Slozitost resoluce

    Resoluce (vyrokova) R je jednoduchy a elegantni dukazovy system pro dokazovani nesplnitelnosti CNF formuli. Jeji verse jsou v zaklade (primo ci neprimo) mnoha systemu pro automaticke dokazovani.

    V seminari se budeme zabyvat tzv. "dukazovou slozitosti" resoluce. Obecnym cilem dukazove slozitosti je porozumet slozitosti dukazu (merene zejmena jejich delkou) v ruznych dukazovych systemech. Delky dukazu odpovidaji casu nedeterministickych algoritmu. Dukazova slozitost je tak dalsim z temat spojujicich matematickou logiku a teorii vypocetni slozitosti.

    Resoluce je jednim z nejlepe prozkoumanych systemu a lze se na ni naucit radu metod vhodnych i ke studiu silnejsich systemu.
    Podivame se zejmena na nektera temata z nasledujiciho seznamu (dle casu):

    obecne cile dukazove slozitosti,
    delka, sire a prostor dukazu v R a jejich vztah,
    spodni a horni odhady na delky dukazu v R,
    tzv. feasible interpolation pro R,
    souvislost prostoru s oblazkovou hrou z t.konecnych modelu,
    kriteria pro spodni odhady v jazyce teorie modelu,
    ne-automatizovatelnost hledani kratkych dukazu,
    zesileni R: systemy R(k) a tzv. "rozsirena resoluce" ER,
    souvislosti s omezenou aritmetikou.

    Misto a cas konani:

    utery 10.4o - 12.1o, seminarni mistnost KA (Karlin, 3.p.)