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