Odporucam pozriet si On the Unusual Effectiveness of Logic in
Computer Science
V akademickom roku 2010/2011 je kurz postaveny na dvoch pilieroch. V ramci
cviceni studenti ziskaju prakticku skusenost s kodovanim problemov do jazka
vyrokovej logiky a s ich riesenim na SAT solveri (najdenim riesenia
povodneho problemu najdenim modelu, kotry splnuje jeho zakodovanie). Viac o tejto oblasti
tejto oblasti vypoctovej logiky v
Satisfiability Solvers . Link na cvicenia .
Prednasky su zalozene na tablovej metode a vychadzaju z knihy Raymonda Smullyana
First Order Logic, ktorej slovensky preklad vysiel v roku 1979.
back
back
back
back
body z midtermu, testu a bonusove body za ulohy z prednasok a minitesty na prednaskach
Vseobecne o kurze
Vypoctova logika sa vyvinula z matematickej logiky a je suborom logickych
disciplin, ktore sa vyuzivaju v informatike a/alebo sa vyuzivaju vo
vypoctovych aplikaciach. Yahrna aj klasicke oblasti logiky, ale pozornost je
sustredena na algoritmicke, vypocotvw apskety. V tejto suvislosti mozeme
zacitovat Kowalskeho alorithmm = logic + control.
Suvisiace kurzy
back
2010/2011
Podmienky pre absolvovanie kurzu
Prednasky
17.2.
oboznamenie s cielom kurzu, s cielom cviceni, s tym, ako vyzera dokaz v
axiomatickych logickych systemoch a ako pri tablovej metode
24.2.
Vyrokkova logika. Formula, vytvarajuca postupnost, vytvarajuci strom. Polska
notacia. Stupen formuly. Strukturalna indukcia. Interpretacia,
model,vyplyvanie.
3.3.
konzistentnost tablovej metody pre vyrokovu logiku: kazda formula
dokaztelna tablovou metodou je tautologia (vrchol kazdej uzavretej tably je
nesplnitelny)
10.3.
uplnost tablovej metody pre vyrokovu logiku - kazda tautologia je dokazatelna tablovou metodou
17.3.
typy uloh na midterm - dokaz, ze formula je trautologia; splnitelnost
mnoziny formul; vyplyvanie formuly z mnoziny formul
prvoradovy jazyk; reprezentacia viet prirodzeneho jazyka v prvoradovom
jayzku; interpretacia
24.3.
pravdivost v interpretacii; model; splnitelnost; vyplyvanie;
31.3.
midterm
7.4.
dokazy tablovou metodou v logike prveho radu
14.4.
nerozhodnutelnost teorem prvoradovej logiky, korektnost a uplnost tablovej
metody
28.4.
ulohy na dokaz platnosti prvoradovej formuly; (ne)splnitelnost mnoziny
formul; (ne)vyplyvanie formuly z mnoziny formul tablovou metodou
5.5.
informativne o niektorych dolezitych temach: kompaktnost; prenexna normalna forma,
prenexne tably, dokazova procedura (tabla je uzavreta akk mnozina formul na
jej jedinej vetve je vyrokovologicky nesplnitelna); Herbrandova
teorema; skolemizacia, rezolvencia; Davis-Putnamov algoritmus
12. 5.
pisomka
Ulohy z prednasok
poslat mailom vzdy do zaciatku prednasky
Hodnotenie
body z cviceni
meno A1 B1 A2 B2 M A3 Z
C H
Belko 3 2 3 2.7 15 18 22.34 D
Benko 5 1.7 15 11 22.34 D
Guzman 0
Heriban 3.5 3.5 2.8 12 15.9
23.4 D
Matkulcik 5 2 2 2.7 15 19.9
23.4 C
Nagy 5 5 2.2 15 25 60 A
Peres 5 2 5 2.9 15 25 61 A
Pukancova 5 5 2.8 15
25 41.49 A
Pukancik 5 2 5 2.4 15 25 37.23
A
Racik 5 5 2.6 9.5 14 48.49 b
Rapcik 5 2 1.9 15 25 34.04 B
Skalicky 5 2 3 15 25 57.4 A
Stupka 1,5 3 9.57
Sipold 3 2 3 2.7 15 25 37.7 B
Sunikova 3 3 2.8 15 4 25 29.79
B
Vladovic 5 0.5 6 10 21.28
E