1. Vybrat z nabízených možností všechny formule, které mohou vzniknout aplikací jedné faktorizace nebo rezoluce

2. Napsat všechny dvojice, které se subsumují (něco takového, tohle jsem si vymyslel…)

a) p(A)

b) p(B) & ~m(B,A)

c) p(f(X)) & ~m(A,A)

d) p(A) & ~m(f(X),c0)

e) p(c0)

3. Převést na klauzuli nebo množinu klauzulí (nějakou takovou, určitě tam byly oba kvantifikátory a „právě tehdy když“:

4. Tablau algoritmus pro formule, které vypadaly nějak takhle:

assumptions:

hypothesis:

5. najděte všechny modely pro 12 prvkovou množinu klauzulí, kde se vyskytovalo 10 neznámých (výroková logika)