Automaticke uvazovani AU zkouska 26.5.2011

60 min - docela malo casu! 
5 prikladu, celkem za 100b, min pozadavek 50+

nebylo to zas tak strasny, spis prakticky priklady, zadna hyperparamodulacni teorie

1/ resolucni metoda (v pred. logice)   (25b)
-dana nekonzistentni soustava klauzuli a my meli dokazat SPOR. 
-bylo potreba delat substituci 

2/ prevest obecnou formuli na klauzuli  (10b)
-zde to byla ekvivalence, (All_X:p(x) <=> Exist_Y:q(y))
-takze skolemnizace, CNF,...

3/ subsumpce  (15b)
-zase mnozina klauzuli, rict ktera subsumuje kterou. 

4/ najit model
-najit dvouprvkovy model, ktery odpovida: 
"# jedna+jedna=jedna
 # All X Ex Y: X+Y!=Y ..."

5/ sestrojit casovy automat (TA), dokazat ze nebudou deadlocky (30b)
-ala mac-kovska mys
-registruje press,release
chceme rozpoznat stavy: 
Click: kliknuti, ktere neni dvojklik
DClick: dve kliknuti za sebou, cas odstup max 500ms
Hold: tlacitko zmacknuto po vice jak 300ms