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ž“:
Tablau algoritmus pro formule, které vypadaly nějak takhle:
assumptions:
exists X r(c0) ⇒ s(X)
exists X s(X) ⇒ r(c0)
hypothesis:
Najděte všechny modely pro 12 prvkovou množinu klauzulí, kde se vyskytovalo 10 výrokových proměnných
Nahoru