== Zkouška 3.6.2015 ==

  - Vybrat z nabízených možností všechny formule, které mohou vzniknout aplikací jedné faktorizace nebo rezoluce 
  - Napsat všechny dvojice, které se subsumují (něco takového, tohle jsem si vymyslel...)
    * p(A) 
    * p(B) & ~m(B,A)
    * p(f(X)) & ~m(A,A)
    * p(A) & ~m(f(X),c0)
    * p(c0)
  - Převést na klauzuli nebo množinu klauzulí (nějakou takovou, určitě tam byly oba kvantifikátory a "právě tehdy když": 
    * all X exists Y p(X,Y) <=> q(X,Y)
  - Tablau algoritmus pro formule, které vypadaly nějak takhle: 
    * assumptions:
      * exists X r(c0) => s(X)
      * exists X s(X) => r(c0)
    * hypothesis:
      * exists X r(c0) <=> s(X)
  - Najděte všechny modely pro 12 prvkovou množinu klauzulí, kde se vyskytovalo 10 výrokových proměnných
~~DISCUSSION~~