courses:au_zk_03_6_15 [OI-Wiki]

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

courses/au_zk_03_6_15.txt · Poslední úprava: 2019/01/10 18:36 (upraveno mimo DokuWiki)

Nahoru