- rozhodnutelnost zastavenia na standardnych a dosiahnutelnych schemach
- prelozitelnosti priechodnych a dosiahnutelnych
- rozhodnutelnost izomorfizmu na volnych schemach
- Porovnajte triedy schem S a R.
- problem zastavenia pre standardne, volne a dosiahnutelne schemy
- Sformulujte a dokazte tvrdenia umoznujuce vyuzit Herbrandove interpretacie
pri dokazovani zakladnych vlastnosti programovych schem.
- Sformulujte a dokazte tvrdenie o (ne)rozhodnutelnosti problemu izomorfizmu
volnych schem. Uvedte definiciu historie vypoctu, pre ktore vase tvrdenie
plati.
{tu moze dat vlastne porovnat alebo rozhodnut hocico}


- Popiste Floydovu metodu.
- rozdiel medzi floydovou a hoareovou metodou z hladiska indukcie
    popisat obe indukcie
- Sformulujte principy konstrukcie spravnych programov vyuzitim Hoareovho
kalkulu.                                           



- Nech C1 a C2 su cpo.
	- Dokazte tvrdenie: ak C1 je diskretne cpo, potom C1 ->s C2 je podm. C1 ->m C2
	- Plati toto tvrdenie, aj ked C1 nie je diskretne cpo? Dokazte, resp. uvedte 
kontrapriklad pre svoje tvrdenie.

- definujte denotacnu a operacnu vstupno vystupnu semantiku. dokazte
ekvivalenciu
- Porovnajte semantiky M a N.
   N je def.:
                 N[while b do S] = najm.horna.hr. fi_i
                 Q_0 = lambda.sigma dolnik
                 Q_i+1 = lambda.sigma if W[b]sigma then N[S](fi_i(sigma))
                                                 else dolnik
- Definicia operacnej semantiky (nie vstupno-vystupna!). Len to bolo menej
zretelne zadane, co vlastne treba urobit...


- zadefinujte bezpecne a korektne vypoctove pravidlo. vymyslite (opiste) vetu o
vytahu medzi nimi a dokazte
- Sformulujte a dokazte vetu o C_p^r a F_p.
- Sformulujte a dokazte tvrdenia, ktore zarucuju, ze semantiku rekurzivnej
definicie mozno definovat pomocou najmensieho pevneho bodu.


- definovat a zdovodnit podmienku ciastocnej spravnosti v relacnom kalkule
    definovat pravidla inferencneho systemu v relacnom kalkule


+ vsetky definicie :)