===== Zkouška AU 26.5.2016=====


  - Zaškrtávací, vybrat formule, které lze z množiny 2 formulí získat jednou aplikací pravidla rezoluce nebo faktorizace. Valná většina byla správně nezaškrtnutá. Množina byla S = {¬ Φ(Y) ∨ π(Y,f(Z)) ∨ π(c0,X); ¬ Φ(Y) ∨ ¬ π(c0,Y)}.
  - Zaškrtávací, z pěti formulí vybrat dvojice formulí, které se subsumují. (Pozn. U subsumpce a rezoluce dejte pozor, že při unifikaci jsou stejně pojmenované proměnné z různých klauzulí ve skutečnosti různé.)
  - Upravit formuli s kvantifikátory a ekvivalencí na množinu klauzulí.
  - Pro teorii najít všechny modely velikosti 2. Teorie byla myslím:
     - (one + one) ~ three Pozn.:Pokud to není zřejmé, + je funkční symbol a ~ predikát.
     - (one + three) ~ one
     - (forall X)(X ~ X)
     - not (one ~ three)
   - Pro teorii z předchozího příkladu vysvětlit, jak úlohu hledání modelu převést na SAT a jak z řešení SAT zpětně zkonstruovat model.