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
Nahoru