navigation
hledat
Rozdíly
Zde můžete vidět rozdíly mezi vybranou verzí a aktuální verzí dané stránky.
|
courses:au_zk_26_5_16 [2016/05/27 09:18] barvijac vytvořeno |
courses:au_zk_26_5_16 [2025/01/03 18:23] (aktuální) |
||
|---|---|---|---|
| Řádek 3: | Řádek 3: | ||
| - | - 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á. | + | - 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é.) | - 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í. | - Upravit formuli s kvantifikátory a ekvivalencí na množinu klauzulí. | ||
| - | - Pro teorii najít všechny modely. Teorie byla myslím: | + | - Pro teorii najít všechny modely velikosti 2. Teorie byla myslím: |
| - | - (one + one) ~ three | + | - (one + one) ~ three Pozn.:Pokud to není zřejmé, + je funkční symbol a ~ predikát. |
| - (one + three) ~ one | - (one + three) ~ one | ||
| - (forall X)(X ~ X) | - (forall X)(X ~ X) | ||
| - not (one ~ three) | - 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. | ||
