AU Zk 23.6.2011

cas tentokrat 2h, coz bylo od nich hezky :)jinak by to sotva slo stihnout. 

uspesnost diky tomu snad vyssi. 

zase 5 uloh, celkem za 100b, min 50.

1/ rezoluce
za 24b, zaskrtavaci policka, spravna odpoved +2, spatna -2b. 
zadana pnozina dvou klauzuli; a rozhodnout, jestli nabizene klauzule mohly vzniknout jednim! krokem rezulucni metody(rezoluce, nebo faktorizace). 

2/ unifikace
za 16b, stejny zaskrtavaci typ; rict, ktere klauzule nejsou subsumovany ostatnimi. 

3/ skolemizace. 
10b, zase checkboxy. (Ex_X: P(x)) <=> (Ex_Y: Q(y))

4/ najit model,
10b; 2 prvkovy, j*j=j   & All_X: ((x!=j) -> x*y!=j)  &  All_X: (Ex_Y: x*y==j))
a kolik takovy modelu je. 
najit model == urcit def. obor a totalni fci. 

5/ prevod na SAT
za 40b!
model ze 4) vhodne popsat a prevest na SAT + jak bychom resili
big-deal uloha